Conversation
…mal orientation kernel-closed
AntiunitaryInvariance.lean (new, 7 results, axiom-clean): no operational
data distinguish the two branches. Transposing the preparation, every
channel (T o G o T), and the effect preserves every circuit probability --
interior transposes cancel in composition and the trace pairing is
transpose-invariant -- for ARBITRARY matrix maps and arbitrary finite
sequences (circuit_invariance), hence for every fixed outcome branch of
any adaptive multi-time strategy, with the instrument outcome-string form
explicit (string_invariance). The transformation is a legitimate symmetry
of the operational formalism: it maps Kraus channels to Kraus channels
with conjugated operators (transposeMap_kraus), preserving complete
positivity by construction and the normalization (kraus_normalization),
and restricted to unitary evolution it is exactly the second branch
(unitary_channel_transpose with BohrFrequency.reflect_conj).
ThermalOrientation.lean (new, 7 results, axiom-clean): oriented thermal
structure is exactly what that symmetry breaks. The antiunitary image of
the +beta Gibbs state of H is the -beta Gibbs state of the reflected
Hamiltonian -- D conj(rho_beta) D^dag = rho_{-beta}(H'), proved in the
reflection branch's own coboundary data (transported_gibbs); +beta and
-beta Gibbs profiles differ whenever two energies differ, coinciding
exactly in the maximally mixed degeneracy (gibbs_orientation); assembled,
a physically fixed positive-temperature Gibbs state excludes the branch
(orientation_excludes_reflection). The passivity layer needs no Gibbs
law: one strictly passive state turns strictly active under energy
reflection (passivity_selector), and positive-beta Gibbs states are
strictly passive -- single-state passivity, strictly weaker than the
complete passivity GR's H-balance discussion locates in the open
composite layer.
Probes: F9 (six-step outcome strings and composed multi-Kraus circuits
invariant to machine precision, partial conjugation breaks it, the
conjugated propagator is the propagator of -conj(H)) and F10 (the
temperature reversal, the matrix identity, the degenerate exception, and
an exact-fraction passivity flip) in bohr_frequency_probe; R7 lint over
all nine Lean files. Ledger records the phase-two structure and the
corpus audit of the orientation question: the classical side derives
beta_E > 0 from horizon counting, the open step is transporting that
orientation across the H-spectrum layer, and the exact fork (A/B) is
recorded as the phase-two target.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
…d in GR 3.3 ThermalOrientation.lean, four new results (all axiom-clean): passive_antipassive_const -- passivity for both orientations squeezes every energy-distinguished pair of populations equal -- and the weak selector passivity_selector_nonuniform: with distinct energies, ONE passive, NON-UNIFORM state excludes the reflection; strictness is not needed. The phase-two physical requirement drops from 'one strictly passive state' to 'one passive, non-maximally-mixed state'. counting_passive and counting_strictlyPassive open the H-orientation transport programme at layer one: exact finite-bath counting with a monotone bath count (beta_E >= 0) makes the counting-selected profile passive for the classical energies -- no Gibbs approximation, no thermodynamic limit. Layers two (stationarity diagonalizes the counting state) and three (energyOrder_transport: the classical exchange ordering agrees with one orientation of the reconstructed Bohr spectrum -- sign only) are the named open targets, the third fork-deciding. papers/GR.md: two corollaries printed immediately after the two-branch theorem -- operational antiunitary invariance (the two branches are two antiunitarily related reconstructions of the same complete circuit statistics, physically distinct only once an oriented structure is fixed) and thermodynamic orientation (reflection inverts thermal orientation; one passive non-maximally-mixed state excludes the branch; Gibbs/KMS sufficient) -- with the split status sentence and the H-orientation question stated but not claimed. The stale prerequisites sentence (iii) now carries the full two-branch residual gauge, and the 3.4 locality proof names both residual freedoms. Both corollaries enter the ledger at K2 with the interpretive glue named in their deltas (127 canonical statements). Appendix Corollary A.3 is flagged in the backlog: its proof cites the 3.3 theorem, which now returns the two-branch form; the sound repair routes through channel equality and phase-locking -- owner's call, untouched this round. Probes: F10 extended with the weak-selector exact check (passive with a tie, non-uniform, fails reflected passivity; the uniform profile survives both orientations; monotone counting yields passivity), F8 lints both corollary headers, R7 covers the four new names. GR rebuilt; full release gate PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
…ing-stationarity audited open
Appendix Corollary A.3 (Hamiltonian consistency) is rewritten in the
two-regime form: at the reconstruction level, equal transition data from
Theorem A.2 give the two-branch conclusion of 3.3 (with the E0 the old
statement omitted); in the exact-unitary regime, equality of the
conjugation actions forces a unimodular scalar between the unitaries and
the spectral phase families then force a mode-independent shift, so
H_dir = H_seq + E0 -- stronger than the old claim: no antiunitary branch
and no nontrivial diagonal, because exact channel equality keeps the
coherence information transition probabilities discard. The closing
sentence records that a general CPTP reduced dynamics has no uniquely
defined Hamiltonian part. Entry GR:C-a.3 rises from GAP to K2.
Kernel, AntiunitaryInvariance.lean (+4, axiom-clean): commute_all_scalar
(the commutant of the full matrix algebra is scalar, by inline
single-entry matrices), ad_eq_scalar (equal conjugation actions force
U = c W with |c| = 1), phase_families_shift and its packaged form (a
common scalar between e^{-iE_a t} and e^{-iE'_a t} at every time is a
single energy shift, by evaluation at t = pi/delta).
Kernel, ThermalOrientation.lean (+4, axiom-clean): commutant_diagonal,
umat_spectral, stationary_offdiag (a state fixed by the evolution at
every time, with distinct energies, has no off-diagonal matrix elements
in the energy eigenbasis -- the phase at t = pi/(Ea-Eb) is -1), and
stationary_spectral_form (a stationary state IS a population profile) --
the mathematical half of transport layer two, exactly the split
requested: stationary_diagonal proved, counting_state_stationary
audited. AUDIT VERDICT (recorded in the ledger route): the joint
counting measure is phi-invariant (Main Lemma 3) and the classical shell
marginal is classically time-invariant, but stationarity under the
RECONSTRUCTED U(t) does not follow from the current construction -- the
shell-counting state is a correlated visible-hidden ensemble while the
Q_fb channel is built on a fixed product prior (GR 3.2's H-shell caveat,
verbatim), and Main Lemma 3's remark confirms prior-dependence. Candidate
routes recorded: the correlated-ensemble projection theorem, or a
quantitative selector absorbing the 1e-123 finite-bath deviation.
Probes: F11 (stationary states are population profiles, generic states
are not; phase multiples share the conjugation action, unrelated
unitaries do not), F8 lints the A.3 strengthening, R7 covers all eight
new names. GR rebuilt; full release gate PASS.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
… both routes converge on the coherent lift ShellAssignment.lean (new, 4 results, axiom-clean): the classical half of the correlated-shell assignment, exact and with no product substitution. Uniform counting on a dynamics-invariant total-energy shell is jointly stationary (shellWeight_invariant / joint_stationary), its visible marginal is stationary on the ACTUAL correlated ensemble (marginal_stationary), and the diagonal-sector assignment map A_shell(|i><i|) = |i><i| (x) mu_H(.|i) is a genuine conditional (shellConditional_sum). The stopping point is hit exactly where directed: representing that assignment inside the coherent reconstructed theory -- a stationary density operator under the reconstructed U(t) whose eigenbasis populations are the classical marginal -- is the first step requiring a new assumption, stated as the named Prop ShellRepresentationConsistency and deliberately not assumed. Downstream of it everything is already kernel-proved. ThermalOrientation.lean (+2, axiom-clean): exists_margin_pair (a passive non-uniform profile has an energy-ordered pair with a strict drop) and approx_passivity_selector (passivity with margin gamma survives any sup-norm perturbation below gamma/2) -- route (b)'s reusable tool, with the guard recorded: the 1e-123 finite-bath number bounds the classical shell-vs-canonical correction, not the represented-vs-shell population distance, and may not be inserted without a new theorem. Probe F12 (exact fractions): an explicit shell with bath counts 1,2,4,8 -- strictly passive marginal, stationarity under a genuinely i-dependent shell-preserving joint dynamics, hidden conditionals on disjoint hidden energy shells, and the margin selector doing real work (the uniform profile beyond gamma/2 is reflected-passive). R7 lints all ten files. Ledger records the convergence verdict: the state route's obligation (extend the assignment into the coherent instrument algebra) and GR 3.2's rate-route obligation (identify the classical shell transition with the frequency-resolved detector transition) are the same coherent operational lift -- the antiunitary-orientation problem is, on this evidence, not an independent gap but another face of the single remaining coherent completion problem in OI -> QM. Full release gate PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
amaybaum
changed the title
amaybaum
changed the title
Item (i): the rate-route conditional is kernelized in ThermalOrientation.lean, deliberately tiny. OperationalTransitionIdentification names the single physical premise (classical exchange rates and reconstructed transition weights share the Boltzmann-ratio form with positive beta_E, tau_K), stated separately and never assumed. Downstream, all axiom-clean: rate_sign_transport (exp injectivity plus positivity transports the sign), energyOrder_transport (the fork-deciding sign correspondence -- the classical energy order is the Bohr-frequency order, conditionally closed), passive_transport, and reflection_excluded_of_transition_identification (OTI => order transport => the reflected orientation admits no passive, non-uniform state). The reduced chains: OTI => energyOrder_transport => reflection excluded, mirroring SRC => stationary spectral populations => reflection excluded. Item (iii): the synthesis is printed in GR 3.3 as the scope paragraph 'One frontier, not two' -- a paragraph, not a theorem. Both routes terminate at single named premises that are two faces of one obligation, the coherent operational lift, so the antiunitary ambiguity is a consequence of the already identified coherent-completion frontier, not an independent incompleteness. Packaging: header docstring updated (layer two half-closed, layer three conditionally closed, the two named premises as faces of one lift); R7 lint extended to the four new results (ThermalOrientation 17 -> 21); LEDGER backlog route updated (rate route reduced, synthesis printed, stale A.3 flag resolved, phase three framed as coherent completion classification: existence of the D_shell representation R with its five conditions, then uniqueness or classification). Full lake build 3015 jobs; three layer probes and the 11-check release gate all pass; census unchanged at 127. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
New file OIBridge/CoherentLift.lean (18 results, all axiom-clean), the C1 package in the process-tensor formulation. Section A, the overlap and the finite comb extension: intersection_consistent kernel-proves the D => Q_fb overlap identity -- the Born branch functional of the permutation lift equals the classical trajectory functional at every horizon and every word over any menu of reversible steps -- via the diagonal invariant qfold_diagonal; previously this equivalence step was certified only numerically (sdq_probes, 1488 realizations at horizons 3-4). finite_comb_extension packages the constructive C1 witness (PSD, trace one, reproduces the classical comb at every word, steps inside Q_fb by construction); branch_normalization is the causal-normalization constraint one slot at a time; extension_forces_agreement / no_common_extension_of_disagreement are the necessity half (one disagreement on the common domain is an infeasibility certificate). Section B, the preparation slot solved exactly. Audit finding, round-critical: the previous ShellRepresentationConsistency (stationarity + prescribed eigenbasis populations) is satisfiable for EVERY profile by the fiat witness V diag(q) V-dagger when V is unitary -- kernel-proved as spectral_clauses_insufficient -- so it under-specified the obligation it names. The Prop is strengthened in place (ShellAssignment.lean): PSD, trace one, stationarity, and the visible restriction rho_ii = p_i; nothing ever assumed the old form, so nothing downstream moves. With the strengthened form: SRC holds iff p = B q for a probability profile q, B_ia = |V_ia|^2 doubly stochastic (shell_representation_from_comb constructive, comb_mixture_of_shell_representation the converse) -- the SDP collapses at the preparation slot to exact linear feasibility p in B(simplex) -- and uniform_overlap_obstruction is the first exact infeasible instance: Fourier-type eigenvectors force uniform visible readout, so the actual F12 shell marginal admits no coherent stationary representation. populations_nonuniform_of_marginal wires non-uniformity through to the selector input. Probe F13 (exact fractions): exhaustive 259-word overlap census to horizon 3, causal normalization on a non-diagonal state, the feasible/infeasible 3-4-5-rotation LP pair with the constructive witness re-verified, the uniform-modulus obstruction on the F12 marginal, and the disagreement countercontrol. R7 lint extended to eleven files (+18 names). LEDGER backlog route records the round and the open C1 residue (multi-time and intervention-algebra conditions against the reconstructed distinct-gap propagator; then C2, then C3 classification). Full lake build 3029 jobs; all probes and the 11-check release gate pass; census unchanged at 127. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
CoherentLift.lean Section C (10 further results, all axiom-clean; 28 in the
file): the rank-one preparation characterization is generalized to Main's
actual carrier -- the ancilla-marginal representation on D = n*m_a with
rank-m_a outcome projectors P_i summing to I, the carrier of the
phase-locking shapes. With B_ia = <a|P_i|a> (projOverlap; nonnegative,
columns summing to one, rows summing to tr P_i -- doubly stochastic with
multiplicity), the projector-valued preparation Prop
ProjectorShellRepresentation holds iff p = B q for a probability profile q,
i.e. iff p lies in conv{B_.a} (projector_shell_representation_from_comb,
comb_mixture_of_projector_shell_representation). Once stationarity and
nondegeneracy are imposed the preparation problem is not an SDP at all: it
collapses to a classical convex-hull condition, and the genuinely quantum
difficulty begins at the multi-time/intervention layer. The rank-one
theorems are the P_i = |i><i| specialization (rankOne_specialization,
projOverlap_rankOne), and the uniform-overlap obstruction generalizes only
under uniform projector overlaps (projector_uniform_overlap_obstruction) --
Section B's Fourier obstruction is carrier-specific.
Probe F14, the decisive census. Exact layer: on structured rational
eigenbases (Pythagorean Givens sweeps, orthogonality verified exactly) the
counting profiles are FEASIBLE at every one of the seven phase-locking
shapes and both mixing depths, with exact Caratheodory certificates -- the
rank-one obstruction does not survive on those carriers; uniform is always
feasible, the deterministic vertex never (max B < 1, exact). Generic layer
(40 seeded Gaussian eigenbases per shape, LP): feasibility depends
systematically on the geometry -- mild non-uniformity representable nearly
always, strong non-uniformity nearly never once n >= 3, the shell profile
splitting both ways at the n = 3 shapes. Verdict recorded in the ledger:
OI-compatible coherent completions are being classified by whether the
shell marginal lies inside their spectral-readout polytope, which
concentration of delocalized eigenvectors shrinks toward uniform.
R7 lint extended (+10 names, CoherentLift 18 -> 28). LEDGER backlog route
records the round and restates the C1 residue carrier-unambiguously:
projector-compatible preparation + distinct-gap U_t + coherent intervention
algebra + causal multi-time consistency. Full lake build 3029 jobs; all
probes and the 11-check release gate pass; census unchanged at 127.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
CoherentLift.lean Section D (25 further results, all axiom-clean; 53 in the file). The guard is structural: every intervention is constrained to the visible factor, J_a = I_a (x) id_A, via the vlift algebra (multiplicative, star-compatible, normalization-preserving); permMatrix_prodCongr and readProj_fst_vlift show Section A's carrier at S = Sv x Sa, pi = fst is the block carrier, so the horizon-k overlap identity already runs on it. Layer one, the classical restriction with the ancilla identity explicit: local_intervention_overlap folds words of lifted classical visible actions and block readouts on block-diagonal states with the ancilla blocks carried untouched (relabelled and masked only); local_intervention_branch reduces the branch probability to the classical fold on the visible alphabet alone. The locality invariant: local_channel_preserves_ancilla -- a visible-local channel preserves the ancilla marginal Tr_V exactly (embedding intertwiner embA_vlift plus trace cyclicity) -- the first hard multi-time constraint of the coherent lift, a consequence of locality alone. The one-slot predicate TwoTimeCoherentLift is stated and never assumed; the Fourier reduction two_time_forces_stationary (Dedekind independence of the gap characters, reusing coeffs_eq_zero / fiber_singleton) plus two_time_necessary collapse it exactly: a two-time lift forces a spectrally diagonal intervened state carrying the classical readout inside the preparation's ancilla-marginal fibre. Probe F15: layer-one exact word census with non-diagonal ancilla blocks; the locality invariant with an ancilla-touching countercontrol; the necessary-LP census (exact) -- the boxed obstruction (globally embeddable, visible-locally impossible) occurs at exactly 8 of 27 strata-x-action instances, block-aligned carriers pass wherever globally feasible; the one-slot Choi problem's exact affine layer -- at (2,2) the problem is RIGID (unique Choi candidate, both hermitian sectors) and fails positivity by a certified macroscopic margin even where the necessary LP passes; the identity action carries the exact identity-channel witness, the aligned carrier is CPTP-completable (Dykstra) on a positive-dimensional instrument fibre; and the probe-menu hierarchy -- permutation and real probes exactly blind to the orientation pair, one complex coherent probe resolves it. R7 lint extended (+25 names, CoherentLift 28 -> 53). LEDGER records the round and the verdict: multi-time visible-local consistency collapses the coherent fibre onto visible-aligned carrier structure, converging with the round-two polytope selection. Full lake build 3029 jobs; all probes and the 11-check release gate pass; census unchanged at 127. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
…ining Three exact closures, in the directed order. (1) New file OIBridge/TwoByTwoNoGo.lean (3 theorems, axiom-clean): the census's sharpest finding is now an exact no-go theorem at an explicit rational witness carrier (G02(3/5)*G23(5/13)*G01(3/5), spectrum (0,1,3,7) with the gap condition decided over the integers, dyadic stationary preparation, transposition action -- preparation feasible by construction and globally reachable). twoByTwo_affine_rigidity: TP + stationarity + readout determine the visible Choi operator uniquely -- sixteen exact linear_combination certificates over the eighteen scalar constraint equations, no positivity used. twoByTwo_nonCP: the unique candidate fails positivity at the explicit vector v = (1,-1,-1,-1) with v^T J v = -449600/76287 -- symbolic, no floating eigenvalue. twoByTwo_no_local_lift assembles both against the named predicate TwoTimeCoherentLift via the round-3 reduction and the new general Choi bridge in CoherentLift Section E (chApply, krausChoi, krausChoi_psd, krausChoi_tp, chApply_krausChoi): preparation feasible + global intervention feasible does NOT imply a visible-local CPTP coherent lift. (2) Reflection blindness derived from phase two, not rebuilt: transpose_conj_response (transpose-symmetric readout and intervened state cannot distinguish U from its entrywise conjugate, by the conjOp transpose identities and trace transposition) and real_instrument_reflection_invariant (real carrier + symmetric preparation + real visible-local instrument gives identical responses under E and -E at every time), with permMatrix_conjOp the permutation special case. The F15 menu table is now structural; a complex probe distinguishes only because it is held fixed rather than transposed -- an externally oriented coherent reference, no violation of antiunitary invariance. (3) Composition closure: ActionIntertwining and ReadoutIntertwining defined, intertwining_all_horizons proves that intertwining at single steps reproduces every finite-horizon branch probability (intertwining_comb_compatible states it against classProb). C1 is now an algebraic representation problem in its final form. Probe F16 recomputes everything exactly: the 18-equation system's rank-16 rigidity, the unique candidate, the negativity witness, readout completeness, distinct gaps, global feasibility; plus the coefficient-level blindness identity and a one-step intertwining check. R7 covers twelve files (CoherentLift 53 -> 66, TwoByTwoNoGo +3). LEDGER records the round and softens the prospective C3 wording per review: aligned-carriers-mod-Z2 is the C3 target, not yet a theorem. Full lake build 3030 jobs; all probes and the 11-check release gate pass; census unchanged at 127. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
C3a executed as directed: define the generated accessible algebra, prove the
trivial-commutant criterion on aligned carriers, and settle what removing the
complex probe leaves behind. New file OIBridge/AccessibleAlgebra.lean
(17 results, axiom-clean).
THE GENERATION THEOREM. accessible_trivial_commutant: for a unitary carrier
with nondegenerate gaps and any operator family whose eigenbasis matrices
N_j = V^H A_j V jointly cover every off-diagonal entry, an operator commuting
with the full-time Heisenberg orbit {U_t A_j U_t^H} is scalar -- the commutant
of the generating set of A_OI is trivial, so by Burnside A_OI = M_D(C). The
proof rewires the round-three engine: each eigen-dyad |v_b><v_a| turns
commutation into one trace expansion (intervened_readout_expansion with the
dyad commutator as readout); singleton fibers give the entry-resolved
equations N_ab (W[b,beta] 1[alpha,a] - 1[b,beta] W[alpha,a]) = 0
(gap_coefficient_vanish, the zero-target Dedekind core; dyad_conjugation, the
exact eigenbasis conjugation); two instantiations kill every off-diagonal of
W = V^H Z V and equalize its diagonal. The completeness hypothesis is
literally hread of two_time_necessary: one alignment datum drives both
stationarity forcing and generation. complexProbe_trivialCommutant is the
requested named specialization (probed visible-local family through vlift).
AUDIT DEVIATION, reported. The expected countercontrol -- removing the
complex probe leaves a nontrivial commutant -- is FALSE in the linear
category: native_menu_generates shows the bare block readouts already
generate on every readout-complete carrier (probe F17, exact: commutant
dimension 1 at the (2,2) no-go carrier and the Fourier carrier for native,
real, and complex menus alike). The true countercontrols, both kernel-proved:
(i) Locality, not menu size: on a sector-decoupled carrier the ancilla phase
diagonal(y o snd) commutes with the whole accessible family of EVERY
visible-local menu, complex probe included (decoupled_carrier_commutes +
ancillaPhase_not_scalar; F17 computes the exact two-dimensional commutant and
identifies it with the ancilla phases). The probe's genuine C3a role is
completeness restoration on blind-but-coupled carriers: at (3,2), two product
eigenvectors sharing an ancilla state leave the native commutant at
dimension 3, and one dense rotated probe restores dimension 1.
(ii) The Z2 residue is antilinear: real_menu_conjugation_stable proves
entrywise conjugation carries each real accessible operator to its
reflected-spectrum twin -- the real menu's accessible family is Theta-stable
even though its linear commutant is trivial -- while the exact unitary
complex probe (probeG_unitary) has a Hermitian response that is a genuine
probed readout (probeResp_is_probe_response) yet is not conjugation-fixed
(complexProbe_breaks_conjugation). The complex probe orients; it does not
generate. This locates phase two's externally oriented reference inside C3
and hands C3b its symmetry group: scalar commutant makes the linear branch
inner, and the antilinear branch is exactly the surviving Theta -- the
Jordan unitary/transpose pair is computed, not imported.
Probe F17 (exact Gaussian-rational fiber equations, float time-sampling
cross-check) censuses commutant dimensions across four carriers x three
menus and verifies every theorem hypothesis in place. R7 covers thirteen
files (+AccessibleAlgebra 17). LEDGER records the round. Full lake build
3031 jobs; both updated probes and the 11-check release gate pass; census
unchanged at 127.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
C3b.1 + C3b.2 as directed, honoring the guard: trivial commutant does not make a data-preserving correspondence inner, so the structure preservation is built exactly. New file OIBridge/OperationalRigidity.lean (17 results, axiom-clean). SEPARATION (C3b.1). operational_separation: an operator invisible to the normalization datum, every one-slot context U_t A_j U_t^H, and every two-slot context U_t A_j U_t^H U_s A_k U_s^H is zero. The proof chains two single-parameter Dedekind extractions: the round-five engine kills every off-diagonal of V^H X V and reduces each two-slot datum to one conjugated entry (conj_context_entry), whose line extraction (line_coefficient_vanish) kills the diagonal. Audit finding, exact in probe F18: one-slot contexts do NOT separate even where the commutant is trivial -- their Fourier-resolved span is 14/16 at the (2,2) census carrier, and two distinct exact stationary states carry identical normalization and one-slot data at every frequency, discriminated only by an explicit two-slot triple (a,b,a). Separation is about temporal depth of the data, not menu completeness. sameData_unique_state then pins the preparation completely: no state-side gauge survives two-slot data. THE DATA-DEFINED MAP (C3b.1). sameData_combination_transfer: identical pairing data against a separating state family transfer linear relations between the two completions' contexts -- the audited well-definedness step. sameData_linear_extension: the C-linear Phi with Phi(G1_i) = G2_i exists, by factoring the linear-combination map through its kernel; no basis is chosen. accessible_cone_full: every positive matrix is a finite selective-word image Sum M_i rho M_i^H of any nonzero positive preparation -- the accessible state cone is the full PSD cone -- and psd_trace_mul_nonneg gives the pairing positivity: the positivity face of the C3b.3 assembly is fully provisioned. KADISON, KERNEL-INTERNAL (C3b.2). orderIso_jordan: a unital R-linear star-preserving bijection of M_D(C), positive in both directions, satisfies Phi(AB+BA) = Phi(A)Phi(B) + Phi(B)Phi(A) on Hermitians. The chain: psd_pair_kernel (interval kernel splitting -- pure positivity, no spectral input), projection_extreme (projections are extreme in [0,1]), extreme_projection (extreme points are projections, by the explicit lambda(1-lambda) eigenframe perturbation on an opaque spectral form), orderIso_maps_projections and orderIso_orthogonal (extremity transport through the two-sided package), orderIso_square (rank-one spectral resolution into pairwise-orthogonal image projections), polarization. Probe F18 checks the Jordan identity exactly on both matrix branches W X W^H and W X^T W^H, and the pinching countercontrol -- positive, unital, not an order isomorphism -- violates it: the two-sided positivity is load-bearing. Remaining for C3b.3: instantiate Phi between two named completions (unitality from the trivial context, star preservation by span induction, two-sided positivity from transfer + cone + pairing positivity), then the unitary/transpose classification on matrix units, with phase two's oriented reference eliminating the transpose branch. Probe F18 (exact); R7 covers fourteen files (+OperationalRigidity 17). LEDGER records the round. Full lake build 3123 jobs; both updated probes and the 11-check release gate pass; census unchanged at 127. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
… matrix-unit classification New file OIBridge/JordanClassification.lean (11 results, all axiom-clean): psd_iff_trace_nonneg (PSD cone self-duality via the rank-one dyad test); sameData_orderIso (the C3b.3 assembly: bijectivity, unitality, star preservation, and two-sided positivity all discharged from operational hypotheses by span induction, so orderIso_jordan fires); the matrix-unit classification chain orthogonal_resolution_rank_one -> corner_form -> corner_nilpotent / corner_unimodular -> corner_cocycle -> orientation_dichotomy -> matrixJordan_unitary_or_transpose (a unital injective star-preserving Jordan map of M_D(C) is X -> WXW^H or X -> WX^TW^H); and the capstone sameData_unitary_or_transpose: any two existing OI-compatible coherent completions with the same complete operational data are unitary or antiunitary equivalent. Probe F19 replays every classification step exactly at D = 3 on both branches with a dense exact unitary, plus the mixed-orientation countercontrol (Jordan fails at the triple (0,1,2)) and the self-duality witness. R7 lint extended to the fifteenth file; ledger round-seven record appended. Full lake build 3124 jobs, both probes green, release gate 11/11. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
…e two orientation routes assembled
New file OIBridge/OrientationSelection.lean (15 results, all axiom-clean;
selector_factorization_invariant depends on no axioms at all).
The selector no-go: the transpose partner ({G^T},{sigma^T}) carries
identical pairing data (transpose_data_eq), is admissible in the same
class (transpose_completion_admissible), and realizes the second branch
with W = 1 (transpose_realizes_second_branch) -- a branch disjoint from
every unitary conjugation (transpose_not_inner). Hence
operational_orientation_noGo: no selector factoring through operational
data can choose the unitary branch -- full unoriented operational data
select QM only up to antiunitary equivalence.
The oriented reference: O with O(Theta R) = -O(R) and OI-derived
O(R) > 0 excludes the transpose partner
(orientedReference_excludes_transpose) and, with the classification,
forces the unitary branch (sameData_unitary_of_orientedReference); such
an O provably cannot factor through Theta-invariant data
(oriented_functional_not_data_definable) -- the oriented datum is an
additional condition, not a consequence of unoriented data.
The two phase-two routes assembled with the classification:
sameData_unitary_of_transitionIdentification (rate route, via
reflection_excluded_of_transition_identification) and
sameData_unitary_of_shellRepresentation (state route, via
shellRepresentation_stationary_profile + passivity_selector_nonuniform).
The remaining foundational question is precise: does bare OI derive
OperationalTransitionIdentification or ShellRepresentationConsistency?
Probe F20 replays the no-go, the disjointness, the margin flip, the OTI
sign transport, and the spectral-profile reconstruction exactly. R7 lint
extended to the sixteenth file; ledger round-eight record appended. Full
lake build 3125 jobs, both probes green, release gate 11/11.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
…c condition can force an orientation New file OIBridge/OrientationClosure.lean (10 results, all axiom-clean; no_universal_oriented_property depends on no axioms at all). The OTI/SRC asymmetry is now a theorem. shellRepresentation_transpose_stable: ShellRepresentationConsistency holds for a model iff it holds for its transpose/reflected partner (V-bar, -E) -- the reflected propagator is the conjugated propagator (umat_reflect_conjM), conjugated sandwiches transpose (conjM_sandwich_transpose), and the visible diagonal survives -- so SRC is an existence condition, not an orientation selector. OTI, by contrast, is genuinely orientation-sensitive (transitionIdentification_orientation_sensitive), and the state-side oriented condition is now named: OrientedShellRepresentation = the SRC clauses + spectral passivity aligned with the energy order + nonuniformity, orientation-sensitive under the carrier nondegeneracies (unitary model, distinct energies, ReadoutSeparating: the moduli mixture pins the spectral profile through stationary_readout). The universal orientation no-go: no_universal_oriented_property -- a Theta-closed inhabited class cannot uniformly satisfy any property with P(R) implying not P(Theta R) -- specialized to both oriented conditions. Bare transpose-symmetric coherent-completion conditions cannot force an orientation: impossible from unoriented data, not merely not yet derived. Probe F21 replays SRC transport (the reflected propagator formally in z-powers), the OTI sensitivity, the pinned shared profile, and the no-go exactly. R7 lint extended to the seventeenth file; ledger round-nine record appended. Full lake build 3126 jobs, both probes green, release gate 11/11. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
…on as a manuscript milestone GR SS3.3: the 'One frontier, not two' paragraph is superseded by 'The coherent-completion classification', separating the three questions with three statuses. Existence: SRC feasibility is the eigenvector-column mixture condition, and the exact (2,2) carrier admits no visible-local CPTP lift -- not every nominal carrier is in the class. Classification: new census theorem (coherent-completion classification), printed with hypotheses verbatim those of sameData_unitary_or_transpose and recorded at K3 -- every two existing completions with identical complete operational data are unitarily or antiunitarily equivalent; no larger coherent fibre. Orientation: new census theorem (operational orientation no-go), also K3 -- transposition preserves admissibility and data, realizes the second branch non-innerly, no data-factoring selector splits the pair, and no inhabited transpose-closed class forces an orientation-sensitive property. The old symmetric SRC-or-OTI fork is retired: SRC files under existence (transpose-stable), OTI and OrientedShellRepresentation under orientation. The two boxed terminal forms carry the existing-completions qualifier. Main SS3.2's gluing remark routes its residual through the classification: what the lift leaves open is existence and orientation, not the size of the family. Ledger: two new K3 entries with named Lean checks; round-ten record. Both papers rebuilt via build.sh (GR 71pp, Main 82pp, no dropped glyphs); release gate 11/11 with staleness green; both probes pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XEQMD5kRhaU9WyeZt6dmM1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
AntiunitaryInvariance.lean (new, 7 results, axiom-clean): no operational data distinguish the two branches. Transposing the preparation, every channel (T o G o T), and the effect preserves every circuit probability -- interior transposes cancel in composition and the trace pairing is transpose-invariant -- for ARBITRARY matrix maps and arbitrary finite sequences (circuit_invariance), hence for every fixed outcome branch of any adaptive multi-time strategy, with the instrument outcome-string form explicit (string_invariance). The transformation is a legitimate symmetry of the operational formalism: it maps Kraus channels to Kraus channels with conjugated operators (transposeMap_kraus), preserving complete positivity by construction and the normalization (kraus_normalization), and restricted to unitary evolution it is exactly the second branch (unitary_channel_transpose with BohrFrequency.reflect_conj).
ThermalOrientation.lean (new, 7 results, axiom-clean): oriented thermal structure is exactly what that symmetry breaks. The antiunitary image of the +beta Gibbs state of H is the -beta Gibbs state of the reflected Hamiltonian -- D conj(rho_beta) D^dag = rho_{-beta}(H'), proved in the reflection branch's own coboundary data (transported_gibbs); +beta and -beta Gibbs profiles differ whenever two energies differ, coinciding exactly in the maximally mixed degeneracy (gibbs_orientation); assembled, a physically fixed positive-temperature Gibbs state excludes the branch (orientation_excludes_reflection). The passivity layer needs no Gibbs law: one strictly passive state turns strictly active under energy reflection (passivity_selector), and positive-beta Gibbs states are strictly passive -- single-state passivity, strictly weaker than the complete passivity GR's H-balance discussion locates in the open composite layer.
Probes: F9 (six-step outcome strings and composed multi-Kraus circuits invariant to machine precision, partial conjugation breaks it, the conjugated propagator is the propagator of -conj(H)) and F10 (the temperature reversal, the matrix identity, the degenerate exception, and an exact-fraction passivity flip) in bohr_frequency_probe; R7 lint over all nine Lean files. Ledger records the phase-two structure and the corpus audit of the orientation question: the classical side derives beta_E > 0 from horizon counting, the open step is transporting that orientation across the H-spectrum layer, and the exact fork (A/B) is recorded as the phase-two target.