Generated deterministically by code/particles/scripts/build_postdiction_ledger.py; the JSON artifact is code/particles/runs/status/postdiction_ledger.json.
Numeric values and measured references on this page are read mechanically from the cited parent artifacts. Structural rows are derived from validated Lean declarations, analytic paper proofs, structured parents, or their combination, and direct algebraic corollaries are identified. The ledger promotes nothing and changes no solve path. Interval rows report containment of the compare-only witness; conditional rows carry their declared premises; chart coordinates keep their NOT_EVALUABLE physical-comparison status.
- The declared twelve-port repair mean selects an intrinsic rank-three Gram quotient as its normalized infinite-response limit. The antipodal-odd integer load quotient is Z^6, the thirty-seam boundary image is the even-sum D6 sublattice, and both signed modules embed densely into the same abstract three-dimensional Euclidean completion. The sixty proper carrier maps act faithfully and isometrically on that completion. This is an exact intrinsic metric completion; physical position, scale, refinement, and gluing are not constructed.
- Complete compact port response from A1 and endogenous overlap transport from A2 force the abstract Lie type su(3)+su(2)+u(1) on the twelve-port carrier. Target-blind readback independently derives R=-J. Inside the declared exterior-response algebra, an exhaustive scan selects the charge-conjugate rank-15 chiral anomaly-free pair and its one-generation hypercharge multiset; its common central kernel is Z6. Source reconstruction of the matrix current and matter action, physical global-form selection, laboratory attachment, and continuum quantum field theory remain separate.
- Every member of the declared positive-weight scalar cosine class, whose full spatial symbol is the orbit sum, has C4 < 0 and B0/C4^2 at least 10/21, with equality exactly on one-radius support. Its anisotropic ranks one through five vanish and B6/B0 lies in [-16/135, 16/75] on the unique rotated I6 line. At eighth order no new angular shape appears, and every one-radius member obeys 5 D6 B0 = 12 B6 D0, equivalently D6/D0 = (12/5)(B6/B0). The polynomial form includes the exact zero-anisotropy mixture; multi-radius members retain radial-moment dependence. The class theorem is exact; physical field attachment, finite scale, coherent frame, readout, and comparison are not constructed.
- Under the balanced-circulant and mass-ordering premises the measured electron and muon masses fix the tau mass inside [1776.968991, 1776.969063] MeV, 0.4336 sigma from measurement. The balance premise is Koide's published relation, which the face circulant of the carrier holds as a finite structure, so this is a conditional postdiction with a frozen rejection rule and a declared premise ancestry.
- The anchor-gap value 0.6379 closes the charged-lepton lane exactly on the measured triple, inside the retrospective accounting interval [0.6199, 0.6506]; the distance +0.0070 to the standard on-shell reference deficit 0.6309 is the scheme unfixed scheme term; scientific owner #736 records that missing source requirement. The lepton scale is localized only under that recorded accounting packet. A source-emitted bridge value is a falsification target: the closure value would satisfy the conditional lane, while a value outside the interval refutes the declared decomposition.
These structural results precede or constrain numeric lanes. They include the icosahedral gauge packet and generic observer-law boundaries. Each row distinguishes analytic paper proofs, finite Lean results and structured executable checks, and records its own classical inputs and missing physical attachments.
| Result | Observed counterpart | Match | Receipts |
|---|---|---|---|
| The certified twelve-port carrier has module 1+3+3'+5 and one fixed line. Complete compact port response from A1 and endogenous proper-carrier transport from A2 force the abstract Lie type u(1)+su(2)+su(3). Target-blind impulse and readback separately determine R=-J. The charged-double-triplet matrices are an exact declared witness, while ordered source tomography and same-current holonomy are not constructed | Standard Model gauge Lie algebra su(3)+su(2)+u(1) | axiom-forced abstract Lie type; conditional matrix witness |
Lean/Screen/A2HolonomyBridge.lean, Lean/Screen/A5OPH.lean, Lean/Screen/A5CharacterField.lean, Lean/Screen/A5SixAxes.lean, code/a5_closure/receipts/port_current_inner_reference.receipt.json |
| The equal-weight cyclic bracket of the twenty pinned oriented faces is exactly 60 times Reynolds basis vector R13 and is A5-equivariant. It fails Jacobi in exactly 240 of the 2640 independent output/input-triple coordinates, split 120 at +1 and 120 at -1. Conditional on the displayed 792-coordinate upper-triangular convention and the certified compact locus, exact primal-dual certificates make G the winning family for three edit norms. Distances to G, F, P are respectively 30(sqrt(5)-1), 60, 60 in L1; (615-123 sqrt(5))/22, (615+123 sqrt(5))/22, 45 in squared L2; and (5-sqrt(5))/10, sqrt(5)/5, 1/2 in Linfinity. The F L1 value is an unattained compact-family infimum | a finite source-incidence discriminator among the three compact bracket families | exact conditional finite discriminator; no source repair law |
Lean/Screen/OrientedFaceBracketSelector.lean, code/b14_jacobi/oriented_face_bracket_selector.certificate.json |
| The carrier splits multiplicity-free into 1+3+3'+5 and the commutant of the port action is exactly four-dimensional, spanned by the four symmetric spectral projectors, so the positive sector-scale cone is the complete family of invariant carrier inner products. Every induced bracket metric is channel-diagonal, and the squared distances from the face bracket to the classified compact families are exact three-term Laurent forms in the sector scales with the fixed-sector scale absent. P is strictly excluded for every invariant metric; every sector-balanced metric and every metric with beta/delta in [1/50, 6] selects G uniquely for all gamma and delta; F occupies the nonempty side d_F^2<d_G^2 of the exact three-scale tie surface, with witness (8,1,1); and Galois conjugation with the sector swap maps d_G to d_F exactly. A non-carrier-induced channel reweighting reverses the balanced-point selection | a metric-robust phase diagram for the finite source-incidence discriminator over the complete invariant carrier-metric cone | exact conditional phase diagram; no source metric or repair law |
Lean/Screen/OrientedFaceInvariantMetric.lean, code/b14_jacobi/invariant_metric_phase.certificate.json |
| For each certified compact bracket, exact ad-invariance of a carrier-projector quadratic form leaves one coefficient per simple factor. The F and G families reduce the three carrier-invariant weights to two: F imposes w(3+)=sqrt(5) w(5), while G imposes w(3-)=sqrt(5) w(5). The P control remains two-to-two. Simultaneous F/G invariance leaves one ray but is an extra mirror-common premise | the finite invariant quadratic-form shape of candidate gauge kinetic terms | exact representation-level finite theorem |
Lean/Screen/GaugeKineticInvariantForms.lean, code/e9_kinetic/gauge_kinetic_invariant_forms.certificate.json |
| For two finite additive step groups, a Gibbs kernel constructed from the weighted sum a q1+b q2 factorizes exactly, and its history action is the corresponding sum of factor actions. If each factor cost has one nonconstant direction, equality of two such constructed transition kernels identifies both multiplier-weighted coefficients; with nonzero multipliers, only one common scaling remains. Exact instances bind both P factors on 3^6 steps and the complete 8+3 dimensional F family on 3^11 steps | a finite multifactor gauge-history action with an identifiable relative kinetic coefficient | exact constructed-kernel compatibility; no independent source law |
Lean/QFT/TwoFactorHistoryBinding.lean |
| The common central kernel on every declared tensor is the order-six diagonal subgroup, so the maximal faithful image of that representation is (SU(3) x SU(2) x U(1))/Z6. The six-axis class has order six only after diagonal and zero-sum coefficient relations are declared. Source selection of those relations, a complete character category, and a same-source loop-to-kernel theorem are not constructed | Standard Model global gauge-group form and its charge quantization pattern | exact conditional kernel and maximal faithful image |
Lean/Screen/Z6Exact.lean, Lean/Screen/Z6Descent.lean, code/a5_closure/receipts/super_tannakian_matter_reference.receipt.json, code/a5_closure/receipts/axis_center_descent_reference.receipt.json |
| Inside the declared 10-component exterior-response algebra, an exhaustive scan of all 1024 subsets selects exactly one unordered charge-conjugate pair of nonempty chiral anomaly-free rank-15 projectors. Primitive determinant balance fixes the block charges up to conjugation, and the selected representative has multiset {Q: 1/6 x6, u_c: -2/3 x3, d_c: 1/3 x3, L: -1/2 x2, e_c: 1 x1}. A separate declared flat classical action assembles gauge, Grassmann-Weyl, Higgs and symbolic Yukawa terms with local Ward and variational-current controls. This ledger checks that packet's custody; its separate full verifier checks the coefficients. A kinetic-aligned local Cartan/Higgs reduction additionally supplies a q5 charged execution with variational current and electric feedback, whose ideal algebra and numerical operation replay are independently checked. A separate exact consumer bounds that action's continuous classical current and spatially distinct intensity response, with every completed-checkpoint intensity error below 6e-6; this is no observed physical postdiction | Standard Model one-generation hypercharge assignment | exact |
Lean/Screen/ExteriorSelection.lean, Lean/Screen/WeylYukawaConventions.lean, code/a5_closure/receipts/super_tannakian_matter_reference.receipt.json, code/a5_closure/manifests/matter_menu_spectral_ledger_reference.json, paper/tex_fragments/LOCAL_SM_JET_ACTION.tex, Lean/Screen/LocalGaugeJetAction.lean, code/sm_local_action/local_action_receipt.json, code/sm_local_action/verify_local_action.py, paper/tex_fragments/CARTAN_SCALAR_REDUCTION.tex, Lean/Screen/CartanScalarReduction.lean, code/sm_abelian_reduction/abelian_receipt.json, code/sm_abelian_reduction/verify_abelian.py, paper/tex_fragments/CARTAN_SCALAR_READOUT.tex, code/sm_abelian_readout/readout_receipt.json, code/sm_abelian_readout/verify_readout.py |
| A supplied finite density state and two Hermitian observables obey the ordinary-commutator Robertson inequality, with exact noncommuting saturation and zero-variance controls. For a supplied projective partition, equality after block pinching is exactly equality of every trace statistic against the full sector-preserving commutant. Partition averaging is the distinct commutative projector-span readout, factors through pinching, is surjective onto the supplied partition's public projector-span algebra, and commutes with the partition commutant. An exact rank-two control keeps the maps distinct. The same pinching is the positive uniform random-unitary average over all 2^k independently signed block reflections. A separate orthogonal-density witness has failed support inclusion but zero raw relative entropy under the totalized matrix logarithm | finite uncertainty, partition-relative superselection, and the support-aware spectral-information boundary | exact bounded finite package; source and physical-instrument attachments not constructed |
Lean/EventAlgebra/Robertson.lean, Lean/EventAlgebra/Superselection.lean, Lean/Screen/B10EdgeCenterAction.lean, Lean/EventAlgebra/RecordMajorization.lean, Lean/EventAlgebra/SpectralEntropyBoundary.lean |
| On the complexified nonzero-momentum transverse fibre, the Fourier-modal block D=i[omega_a(k)/|k|](k cross -) has zero modal divergence and squares to the committed FZ-12 scalar spatial action. The opposite-sign pair G(E,B)=(D B,-D E) therefore squares to the existing second-order oscillator on both amplitudes; the same-sign mutation has the wrong second-order sign | Fourier-modal algebra of the vacuum Maxwell curl pair; not a physical electromagnetic observation | exact bounded modal factorization; local source-produced physical Maxwell theory not constructed |
Lean/Screen/ModalMaxwellFactorizationBoundary.lean, code/electromagnetism/modal_maxwell_factorization.py, code/electromagnetism/test_modal_maxwell_factorization.py, paper/screen_microphysics_and_observer_synchronization.tex |
| In every Hausdorff topological group, ordinary convergence of the natural powers g^n forces g to be the identity. Thus a supplied nonidentity finite-dimensional exact unitary U at fixed cutoff has no ordinary large-time limit in either the unitary subgroup or the ambient matrix topology, and hence has no full weak-operator limit at that same fixed finite dimension. The exact scope control (U^n)^(-1) U^n = 1 converges for every U | fixed-cutoff scattering-construction boundary; not a physical observation or prediction | exact direct-power obstruction; physical scattering and asymptotic comparison construction not constructed |
Lean/QFT/FiniteUnitaryScatteringNoGo.lean, code/qft/finite_unitary_scattering_no_go.py, code/qft/test_finite_unitary_scattering_no_go.py, paper/tex_fragments/QFT_STRUCTURAL_INHERITANCE_STATUS.tex |
| The Mathlib exterior basis on the declared five-mode carrier has 32 labels and binds the ten non-vacuum, non-top component rows to their dimensions, charges, parity, conjugation, square-zero creation, and anticommutation. One explicit typed map assigns those rows to supplied partition sectors and central weights. The supplied weights define a sixth-root character action on the component-labelled finite product of mapped projector ranges with the exact six-element tensor kernel. The supplied anomaly-free exterior-degree parity support is nontrivial, invariant, and detects the same kernel | finite exclusion and one-generation central-weight structure | exact bounded finite action; source selection and physical matter attachment not constructed |
Lean/Screen/ExteriorComponentBridge.lean, Lean/Screen/QuantumMatterIntegration.lean, Lean/Screen/B10EdgeCenterAction.lean |
| A5-invariant readouts have port-independent group-averaged cap sums, so the per-cap ratio of any two averaged readouts is universal with zero spread | universality clause of the Einstein-branch coupling law | structural |
Lean/Screen/A5CouplingSymmetry.lean, Lean/Screen/A5PortAction.lean, Lean/Screen/PortFrameGram.lean |
| The declared twelve-port repair mean selects an intrinsic rank-three Gram quotient as its normalized infinite-response limit. The antipodal-odd integer load quotient is Z^6, the thirty-seam boundary image is the even-sum D6 sublattice, and both signed modules embed densely into the same abstract three-dimensional Euclidean completion. The sixty proper carrier maps act faithfully and isometrically on that completion | a three-dimensional local spatial carrier with proper icosahedral frame changes | exact intrinsic metric completion; physical position, scale, refinement, and gluing not constructed |
Lean/Screen/PortGramRepairBand.lean, Lean/Screen/PortGramRepairCovariance.lean, Lean/Screen/PrimitivePortFrameQuotient.lean, Lean/Screen/RepairWordCarrierReadout.lean, Lean/Screen/SeamCurrentCarrierQuotient.lean, Lean/Screen/PortGramA5Isometry.lean |
| On a supplied finite directed graph with an integer layering, a finite depth, steady sourcing, shell equidistribution, and shell cardinality c n^2, exact divergence bookkeeping gives outward flux per shell edge Q/(c n^2) and makes flux times n^2 shell-independent. A three-vertex chain inhabits the premises. Two exact global controls show why the depth bound is essential: a globally steady drained source on a closed finite carrier has zero total load, and an n^2 shell law at every positive layer forces c=0 | a depth-bounded discrete inverse-square precursor with no physical radius, gravitational-field, or mass identification | exact conditional finite theorem under PR-29, PR-30, and PR-31; physical Newtonian attachment not constructed |
Lean/Screen/LayeredDiscreteGauss.lean |
| Every member of the declared positive-weight scalar cosine class, whose full spatial symbol is the orbit sum, has C4 < 0 and B0/C4^2 at least 10/21, with equality exactly on one-radius support. Its anisotropic ranks one through five vanish and B6/B0 lies in [-16/135, 16/75] on the unique rotated I6 line. At eighth order no new angular shape appears, and every one-radius member obeys 5 D6 B0 = 12 B6 D0, equivalently D6/D0 = (12/5)(B6/B0). The polynomial form includes the exact zero-anisotropy mixture; multi-radius members retain radial-moment dependence | a linked isotropic and rank-six vacuum-dispersion surface not fixed by the Standard Model with General Relativity | exact class theorem; physical sector, frame, finite scale, readout, and comparison not constructed |
Lean/Screen/A5CarrierClassBand.lean, code/a5_fingerprint/runtime/carrier_class_dispersion_receipt.json |
| Every normalized complete positive tight-frame cosine symbol has an exact sine-feature realization. The feature map is a Euclidean contraction, so its nonnegative auxiliary frequency is globally 1-Lipschitz at all momenta. Exact support bindings give t=4 and prefactor 1/(2a^2) for the FZ-11 vertex support, and t=10 and prefactor 1/(5a^2) for the FZ-12 edge support | an all-momentum upper bound on an auxiliary carrier dispersion | exact bounded finite theorem; physical position, frequency, clock, field, signal front, frame, scale, readout, and comparison not constructed |
Lean/Screen/CarrierFrequencySpeed.lean, code/a5_fingerprint/runtime/carrier_frequency_speed_receipt.json |
| Universe closure, repair execution order, observer record order, modular parameter, worldline realization, clock readout, proper time, and optional global time are distinct formal types. In the committed source environment, a canonical witness matrix rejects all 56 ordered transitive coercions between distinct layers, and explicit named maps are required. Positive affine clock regraduation preserves strict record monotonicity, and an inhabited record with nonzero offset proves clock-origin nonuniqueness | typed separation between operational ordering and physical time | exact formal boundary; physical time realization not constructed |
Lean/Time/TimeOrderLedger.lean |
| A record history with a supplied strictly increasing natural-number rank gives an order-compatible scalar readout, which admits every strictly increasing regrading; an exact three-tick cubic control is not affine. After a unit-timelike affine event law is supplied, every precedence is future timelike across overlapping charts and along that same supplied history the positive clock increment is additive with square equal to the invariant Lorentz quadratic interval. One shared event leaves an affine comparison nonunique; two ordered event pairs determine the unique positive-affine interpolation of their four supplied readings. At a third shared event, affine consistency is equivalent to a cross-product equation and gives a nondegenerate no-new-fit-parameter check when its event and both readings differ from the anchors. A held-out reading requires separate predesignation and custody | record-order data and conditional operational clock comparison | exact bounded conditional algebra with finite controls; source physical clock not constructed |
Lean/Time/ObserverHistory.lean, Lean/Time/ClockReadout.lean, Lean/Time/WorldlineRealization.lean, Lean/Time/ProperTimeCalibration.lean, Lean/Time/ClockComparison.lean |
| The span of a finite projective partition is a commutative matrix star subalgebra contained in its commutant and is star-algebra equivalent to complex functions on the nonzero projector labels. A common linear isometry can sharply copy two distinct states from one normalized blank only when they are orthogonal | classical public records and the sharp-state copying boundary | exact finite theorem package |
Lean/EventAlgebra/PublicRecordAlgebra.lean, Lean/EventAlgebra/NoBroadcastingAdapter.lean |
| One typed directed refinement object carries finite observer and record fibres, observer record orders, private matrix algebras, commutative public star subalgebras, record representatives, certified states, and linear generators. Its refinement laws preserve every layer, with states restricting contravariantly by exact trace pairing. A constant adaptor reuses an existing projective partition and density state with discrete order and zero generator | one common finite refinement substrate for observer theories | exact structural interface; source realization not constructed |
Lean/Tower/ConsensusTower.lean |
| A finite inhabited raw presentation has a literal kernel quotient whose equality is exactly public-readback equality and whose points are the realized signatures. Termination constructs a finite completed schedule; confluence, semantic fixed-point completeness, and explicit repair-output plus enabledness congruence make the consistent public endpoint independent of completed schedule and raw representative. The existing OPH Repair descends to an idempotent public map, and typed OPH and A3-regulator adaptors retain every premise | an observer-independent public normal-form endpoint | exact bounded conditional endpoint; source and limit not constructed |
Lean/Tower/PublicWorldQuotient.lean, Lean/Tower/FixedPointEndpoint.lean |
| The real Pauli-coordinate module Herm2 is exactly the four-dimensional space of two-by-two complex Hermitian matrices, with determinant equal to the Lorentz quadratic form of constructive inertia (+---). Positive future-null rays are set-equivalent to the unit two-sphere, the algebraic future-unit hyperboloid has three-dimensional positive rest spaces, and an explicit linear chart matches the existing Einstein coordinates with exactly the required sign flip | four-dimensional ambient Lorentz module and observer-frame algebra | exact ambient module algebra and coordinate bridge; source-causal event attachment and physical soldering remain outside C1 |
Lean/Geometry/CanonicalLorentzModule.lean, Lean/Geometry/CelestialNullCone.lean, Lean/Geometry/ObserverFrameHyperboloid.lean, Lean/Geometry/ObserverRestSpace.lean, Lean/Geometry/EinsteinTensorBridge.lean |
| Authenticated read-after-write provenance generates a finite locally finite partial order, and canonical source height obeys the exact longest-parent-path recursion. Independently of that order, an independent real axis and the proved rank-three source Gram quotient define an exact four-dimensional carrier with signature (+---); every source-unit spatial direction gives a future-null vector. A supplied positive time scale and spatial readback use source height only in the event placement. With the parent-edge speed bound, generated precedence maps into the carrier future cone. A separately certified faithful placement upgrades this to two-way order--cone equivalence and constructs the finite source-order/frame packet. The explicit four-event Boolean diamond is a non-chain control whose generated order agrees exactly with its carrier cone order. A separate supplied growing-menu lattice has exact finite inner/outer cone bounds and an analytic controlled cone and interval-volume limit; its local read/write control has 81 events, 794 authenticated edges and width 27. A separate conditional construction selects finite populations from the dense source metric and gives a positive scalar action with an analytic continuum field and detector error bound; physical selection of the coarsening and action is not derived. A declared local-read law on golden-orbit conservative source records has Lean-constructed finite cone bounds and analytic raw-count four-volume and contained-interval ordering-fraction limits, the latter equal to 1/10. Independent exact finite executions use 27, 125, 512 and 2197 sites with equal widths; the sharper q=13 fill gives inner speed at least 75989/250000. On this declared family, fourth roots of authenticated interval-count ratios recover geometric proper-time ratios, uniquely up to units among positive volume-only inertially additive readouts. Exact q=5 replay checks the decoder. A separate analytic finite-rotation/one-boost criterion selects the Lorentz cone under operational covariance. The same declared scalar action has controlled spacetime-smeared boost comparisons for two reference-supplied preparations. A separate protected-address experiment exactly distinguishes immutable records from moving live readbacks under pair means. Formal integrated cell estimates derive quadrature convergence from vanishing assignment distances. Fibonacci arithmetic constructs the actual golden permutation partition, its exact cell masses and fixed-globally-Lipschitz integral convergence in Lean. Actual spatial and declared-time-grid counts also converge on fixed measurable sets with null frontier; the inclusive final-layer error is at most L^3Delta_q. On the same prepared golden coordinates, a different local massive Dirichlet scalar action has an analytic free-field detector limit and a finite full-Fock compact detector response whose exact certified error is smaller than its signal. For that action, stable local time refinement converges to the same detector limit; nearest-update readout preserves a resolved finite comparison, and the preparation-induced response vanishes asymptotically before continuum arrival. In a separate 64-site execution, graph-recovered configurations determine positive durations for a supplied action family; conditional timing intervals retain 15 of 21 resolved fixed-state quantum predictions. A sharp kernel criterion also identifies the minimum exterior linear readouts needed to reconstruct the original regional canonical algebra from two field layers; eight exact regional controls retain every exterior coupling. Separate canonical-mean path calibrations reconstruct remote initial data from destination samples alone, with all 1449 events and their precision costs retained. Their all-depth infinity-norm condition number obeys the exact recurrence g_0=1, g_1=3, g_d=2g_(d-1)+g_(d-2); a separate sufficient bound propagates supplied gate, retained-sample and decoding errors. With supplied local copy/reset and factor-two readback, reusable version transport instead has unit per-hop signal gain and a sharp linear additive error bound; 4928 events retain exact semantic order and old-version reads. A separate centered quantum instrument includes all earlier-readout backaction in 21 unconditional marginals and retains 15 resolved comparisons against continuous evolution under that same repeated instrument. An exact finite rectangular pointer pulse keeps field evolution active; bounded pulse duration and declared channel noise retain all fifteen responses when both baseline and intervention errors and all control windows are counted. These results do not identify a physical clock or select native field dynamics | finite causal-set-like order with an effective 1+3 Lorentz carrier and null-cone directions | exact source-derived finite order and 1+3 carrier theorem stack; physical faithful placement and continuum manifold not constructed |
Lean/ObserverPatchHolography/Provenance/CausalInterval.lean, Lean/ObserverPatchHolography/Provenance/SemanticEventProvenance.lean, Lean/Geometry/SourceDerivedSpacetimeCarrier.lean, Lean/Geometry/SourceOrderFrameCompatibilityPacket.lean, Lean/Geometry/SourceRecordProtection.lean, Lean/Geometry/SourcePopulationQuadrature.lean, Lean/Geometry/GoldenSourceAssignment.lean, Lean/Geometry/GoldenSourceCountLimit.lean, Lean/Geometry/SourceFeedbackTransport.lean, paper/tex_fragments/SOURCE_FEEDBACK_TRANSPORT.tex, code/source_feedback_transport/transport_receipt.json, code/source_feedback_transport/verify_transport.py, paper/tex_fragments/SOURCE_SCALAR_SEQUENTIAL_INSTRUMENT.tex, code/source_scalar_instruments/sequential_instrument_receipt.json, code/source_scalar_instruments/verify_sequential_instrument.py, paper/tex_fragments/SOURCE_SCALAR_FINITE_INSTRUMENT.tex, code/source_scalar_finite_instrument/finite_instrument_receipt.json, code/source_scalar_finite_instrument/verify_finite_instrument.py, Lean/Geometry/SourceSeamPathTomography.lean, paper/tex_fragments/SOURCE_SEAM_PATH_TOMOGRAPHY.tex, code/source_routing/runtime/path_tomography_receipt.json, code/source_routing/verify_routing.py, Lean/QFT/ScalarRegionalTimeSlice.lean, paper/tex_fragments/SOURCE_SCALAR_REGIONAL_TIME_SLICE.tex, code/source_scalar_regional/regional_time_slice_receipt.json, code/source_scalar_regional/verify_regional_time_slice.py, paper/tex_fragments/SOURCE_RECORD_PROTECTION.tex, paper/tex_fragments/SOURCE_POPULATION_QUADRATURE.tex, code/source_population/runtime/population_receipt.json, code/source_population/verify_population.py, paper/tex_fragments/SOURCE_COMMON_SCALAR_PACKET.tex, code/source_scalar_packet/source_common_scalar_receipt.json, code/source_scalar_packet/verify_source_common_scalar.py, paper/tex_fragments/SOURCE_SCALAR_EXECUTION.tex, code/source_scalar_execution/source_scalar_execution_receipt.json, code/source_scalar_execution/verify_source_scalar_execution.py, paper/tex_fragments/SOURCE_SCALAR_QUANTUM.tex, code/source_scalar_quantum/quantum_probability_receipt.json, code/source_scalar_quantum/verify_quantum_probability.py, paper/tex_fragments/SOURCE_SCALAR_CLOCK.tex, Lean/Screen/ActionTimeGram.lean, Lean/Screen/SourceActionTime.lean, code/source_scalar_clock/source_scalar_clock_receipt.json, code/source_scalar_clock/verify_source_scalar_clock.py, paper/tex_fragments/SOURCE_SCALAR_CLOCK_QUANTUM.tex, code/source_scalar_clock_quantum/clock_quantum_receipt.json, code/source_scalar_clock_quantum/verify_clock_quantum.py, paper/tex_fragments/SOURCE_SCALAR_TIME_REFINEMENT.tex, code/source_scalar_time_refinement/source_scalar_time_refinement_receipt.json, code/source_scalar_time_refinement/verify_source_scalar_time_refinement.py, Lean/Geometry/MetricKernelEnergy.lean, paper/tex_fragments/SOURCE_METRIC_SCALAR_CONTINUUM.tex, Lean/Geometry/RefiningLatticeCausalCone.lean, paper/tex_fragments/REFINING_CAUSAL_CONE.tex, code/causal_refinement/refining_cone.py, code/causal_refinement/verify_refining_cone.py, code/causal_refinement/test_refining_cone.py, code/causal_refinement/refining_cone_receipt.json, Lean/Geometry/SourceNetCausalCone.lean, paper/tex_fragments/SOURCE_NET_CAUSAL_LIMIT.tex, code/causal_refinement/source_net_causet.py, code/causal_refinement/verify_source_net_causet.py, code/causal_refinement/test_source_net_causet.py, code/causal_refinement/source_net_causet_receipt.json, paper/tex_fragments/OPERATIONAL_CAUSAL_SELECTION.tex, paper/tex_fragments/SOURCE_COUNT_CLOCK.tex, Lean/Time/SourceCountClock.lean, code/causal_refinement/source_count_clock.py, code/causal_refinement/verify_source_count_clock.py, code/causal_refinement/test_source_count_clock.py, code/causal_refinement/source_count_clock_receipt.json |
| Coincidence-invariant Herm2 readback descends uniquely through an actual event setoid. Separately, one supplied time-oriented affine Lorentz overlap cocycle and a chart-coordinate family satisfying its overlap law induce translation-free displacement covariance, invariant intervals, future-null celestial transport, compatible event frames, and isometric transport of their positive rest spaces. The rank-three source FrameQuotient is linearly and isometrically identified with the standard internal rest fiber as a candidate local readback. The formal stack does not identify the quotient-descended readback with the supplied atlas coordinates. Exact controls exhibit a nontrivial translated future-null atlas and show that reflexive symmetric pairwise overlap need not be transitive | event-frame and local rest-space Lorentz covariance | exact bounded algebraic contract; source and physical receipts not constructed |
Lean/Geometry/LorentzOverlapCocycle.lean, Lean/Geometry/EventGermDisplacement.lean, Lean/Geometry/CelestialSoldering.lean, Lean/Geometry/EventFrameSoldering.lean, Lean/Geometry/SpatialReadbackSoldering.lean |
| A proof-carrying finite enrichment of one consensus tower has declared region posets, overlaps, disjointness, local star subalgebras, isotony, algebraic locality, covariant refinement, compatible expectations, and idempotent regional repairs that explicitly fix local and declared-disjoint observables. Its relaxations compose exactly and preserve remote expectations. Supplied overlap restrictions support a unique restriction-gluing interface on declared nonempty subregion families, controls isolate missing premises, and a partition-and-state-parameterized commutative model proves conditional consistency. A retained source packet supplies four disjoint windows with split-fibre labels; a separately declared adapter constructs noncommutative regional blocks, exact coverage and gluing, and nonunital two-by-two matrix corners at every window. A five-module continuation conditionally proves full observer-algebra generation from post-hoc counted transitions and field projectors, exact commuting factors on a declared Cartesian carrier, a conditional-expectation diamond with coverage and an explicit noninjective-correlation control, and transport to one constant A3 stage on the distinct 86/88 carrier. The 86/247 capstone kernel-checks fully disjoint source supports and an exact counted correlated state with the committed marginals on the instantiated diamond | a causal local quantum-observable net with overlap descent | substantial conditional finite interface, operator-generation, CP-diamond, and support-disjoint counted-correlation packet; source justification of the factor reading and a nonconstant realization are not constructed |
Lean/QFT/FiniteCausalObserverNet.lean, Lean/QFT/ObserverNetDescent.lean, Lean/QFT/RichFibreWitness.lean, Lean/QFT/RichFibreRegionalNet.lean, Lean/QFT/SourceOperatorGeneration.lean, Lean/QFT/JointSlotFactorisation.lean, Lean/QFT/CPRestrictionNet.lean, Lean/QFT/TwoSlotCPNetWitness.lean, Lean/QFT/TowerAnchoredDiamond.lean, Lean/QFT/SourceCorrelationCapstone.lean, Lean/QFT/StructuralNetAdequacySurface.lean |
| An idempotent linear publicization map has an exactly solvable public-residual relaxation with multiplicative composition and exponential semigroup law. Its Poissonized closed form satisfies the initial-value and generator-flow identities and equals the literal Banach-algebra operator exponential for bounded idempotent endomorphisms. Partition averaging has an explicit normalized Kraus family and is formally CPTP. Partition pinching is also CPTP, and its generator equals the displayed projector-rate matrix dissipator with fixed algebra equal to the commutant at nonzero rate | finite public/private relaxation and stable pointer algebra | exact finite linear and matrix identities |
Lean/EventAlgebra/PartitionAverageCP.lean, Lean/EventAlgebra/TwoScalePublicRepair.lean, Lean/Thermodynamics/PoissonizedRepair.lean, Lean/Thermodynamics/PoissonizedRepairOperatorExp.lean, Lean/Dynamics/ConditionalExpectationGenerator.lean, Lean/Dynamics/ChoiCPTP.lean |
| Positive unital complex-linear maps of the finite active-record function algebra are exactly real row-stochastic kernels under the declared coordinatewise cone. Every public star automorphism is uniquely pullback by a label permutation, so every pointwise-continuous real-parameter group of arbitrary public star automorphisms is trivial. Every star automorphism of one finite full private endomorphism block is unitarily inner, and a supplied self-adjoint Hamiltonian generates a unitary real-parameter von Neumann flow | classical-stochastic public and quantum-unitary private dynamics | substantial exact finite packet; global converse not constructed |
Lean/Dynamics/PublicMarkov.lean, Lean/Dynamics/PublicAutomorphism.lean, Lean/Dynamics/PrivateInner.lean |
| For reversal-compatible group labels on endpoint-typed finite paths, the ordered transport ratio of two common-endpoint paths equals the holonomy of their closed ratio loop, and every unitary character maps it to the exact relative phase. Recharting conjugates based holonomy and leaves character phase invariant. An explicit four-vertex path/face control has two flat declared triangular faces and a separate undeclared, unfilled loop with nontrivial holonomy and two-arm phase. A supplied cyclic ZMod n sector forces the character phase to be an nth root of unity | finite algebraic two-path character phase and cyclic-root structure | exact bounded algebraic packet; physical attachment not constructed |
Lean/Screen/HolonomyInterference.lean |
| At one finite regulator, two distinct operational observers can be bound through the E6 access cut so that each owner algebra is the declared accessible algebra, every committed record and own readout agrees after typed restriction to a proper meet, and one common restriction is nonzero and accessible to both. In the exact witness, owner-region records differ before restriction and agree only at the shared corner; a one-corner mutation falsifies the receipt | the seven-clause bounded operational-observer and shared-record interface | exact fixed-regulator witness and negative control |
Lean/QFT/OperationalOverlapEvidence.lean |
| The twelve declared central port atoms form one classical context with an eleven-dimensional normalized weight simplex. The separate declared qubit adapter has six disjoint antipodal binary contexts: additive weights have affine dimension six, while the trace-one Hermitian/Born slice has dimension three and is characterized by three exact golden-ratio relations. Tomography is unique when a representation exists, but exact unit-interval controls show both nonrepresentation and a unique Hermitian representation whose matrix is nonpositive. On the full celestial sphere, the continuous normalized binary weight F(n)=(1+n_z^3)/2 is exactly non-affine; after affinity is supplied, dense probability tests force the coefficient into the closed unit ball. The displayed finite unsharp battery also fails: F_y(n)=(1+n_y^3)/2 is normalized, probability-valued, noncontextual on the whole web, and non-affine. The source-attached real S3 algebraic contexts obtained by applying a declared representation to source-realized gauge labels are not complex tomographically complete: distinct pure Pauli-Y states agree on every declared outcome and a missing complex Y projector separates them. For two source-attached algebraic projector candidates P,Q, the algebraic phase lift I/2-(2sqrt(3)/3)i(QP-PQ) is exactly that Y projector and completes fixed-trace tomography; every effect in a generous real/Kraus closure remains Y-blind and cannot produce it. Entrywise conjugation exchanges the two phase candidates while simultaneous state-effect conjugation preserves the real Born weight. A post-hoc raw-count product-gap diagnostic from retained B12 data supplies an exact reversal-odd bit and normalized cycle products, but neither its statistic nor designation rule was preregistered; its pairing with the phase torsor is declared and emits no source selection or validation | finite noncontextual weight representation and the Born rule | exact bounded rank-gap and phase-free no-gos plus an algebraic complex tomography target; public quantum instrument missing |
Lean/EventAlgebra/FiniteBornFrame.lean, Lean/EventAlgebra/FiniteEffectClosureBoundary.lean, Lean/EventAlgebra/FiniteWebBornNoGo.lean, Lean/QFT/SourceContextTomographyNoGo.lean, Lean/QFT/SourcePhaseLiftBridge.lean, Lean/QFT/ConjugationGauge.lean, Lean/Thermodynamics/RepairCurrentOrientation.lean, Lean/QFT/SourceOrientedCompletion.lean, code/born_frame/runtime/finite_born_frame_certificate.json, code/born_frame/verify_finite_born_frame_independent.py, code/born_context_phase_lift/BORN_CONTEXT_WEB_PAYLOAD.v1.json, code/born_context_phase_lift/README.md, code/born_context_phase_lift/verify_source_phase_lift.py, code/born_context_phase_lift/test_source_phase_lift.py, code/thermodynamics/repair_current_orientation/repair_current_payload.v3.json, code/thermodynamics/repair_current_orientation/verify_repair_current_orientation.py, code/thermodynamics/repair_current_orientation/test_verify_repair_current_orientation.py |
| With a faithful common reference and repaired-visible fibre supplied, Axiom 3 instantiated on states selects the Gibbs exponential family by the exact information-projection Pythagorean identity, and instantiated on transition distributions over the repaired-visible fibre selects weighted conditional resampling from the same reference. The kernel is stochastic, idempotent, reversible, stationary, and fixes fibre-measurable charges; relative entropy to the reference contracts under it; the exact first-law split carries its bilinear cross term; the excited Gibbs mass obeys the finite gap bound with entropy limit log g0; partition pinching has an explicit normalized projector Kraus family and is formally CPTP; more generally, every stochastic kernel preserving a faithful stationary reference contracts relative entropy even without detailed balance, with an exact lazy directed three-cycle as the nonreversible separation witness. On the committed source artifact, however, the transition action has a nonconstant eigenmode with eigenvalue 665437/726948, whereas the candidate state-side heat-bath action is idempotent; every intertwiner kills that mode. Its stationary mass 7155/61511 is also not a deterministic pushforward of the equally weighted 16384-state empirical table | the zeroth, first, second, and third laws of thermodynamics | finite theorem package under named receipts |
Lean/Thermodynamics/FiniteConditionalRepair.lean, Lean/Thermodynamics/StationaryRealization.lean, Lean/Thermodynamics/FirstLawIdentity.lean, Lean/Thermodynamics/FluctuationTheorems.lean, Lean/Thermodynamics/CapFirstLaw.lean, Lean/Thermodynamics/EinsteinPremiseLink.lean, Lean/EventAlgebra/PartitionPinchingCP.lean, Lean/Dynamics/ChoiCPTP.lean, Lean/Thermodynamics/CommonReferenceObstruction.lean |
| A finite reversible Markov kernel with a linear Poisson solver has a symmetric positive-semidefinite Green--Kubo matrix and an exact finite correlation sum with propagated remainder. One full-fibre repair projector has constant positive-lag correlation and cannot supply a nonzero decaying memory tail with stabilizing sums. Typed finite-graph Fick and Fourier updates obey exact source balance and source-free conservation. A separate exact eight-state supplied local resampling law preserves a nonconstant record while its fibre-centred currents have decaying memory, a gap of at least 7/192, and a rational Green--Kubo matrix with certified tails | Onsager symmetry, Green--Kubo response, Fick diffusion, and Fourier heat transport | exact finite conditional transport structure; physical generator and coefficients not constructed |
Lean/Thermodynamics/GreenKubo.lean, Lean/Thermodynamics/GraphDiffusion.lean, code/thermodynamics/protected_memory/protected_memory.py, code/thermodynamics/protected_memory/verify_protected_memory.py, code/thermodynamics/protected_memory/test_protected_memory.py, code/thermodynamics/protected_memory/runtime/protected_memory_receipt.json, paper/tex_fragments/PROTECTED_RECORD_MEMORY.tex |
| On the exact twelve-port, thirty-seam incidence graph, a declared pointwise continuity update gives regional source minus outward flux, internal cancellation, and closed-graph conservation for zero-total source. Rational Gauss solutions exist exactly for neutral loads and form one translate of a nineteen-dimensional cycle kernel. For finite real linear state maps, all-state charge conservation is equivalent to the dual fixed-observable equation; an exact two-state counterexample shows that channel covariance alone does not imply conservation | continuity, Gauss constraint, and protected-charge structure | exact finite precursor; physical Ward bridge not constructed |
Lean/Screen/RegionalContinuity.lean, Lean/Screen/DiscreteGauss.lean, Lean/Dynamics/ProtectedCharge.lean, Lean/Dynamics/WardLimitManifest.lean |
| For the concrete single-site OPH localRepair, every fixed exogenous word of n sequential moves has an n-fold closed-neighborhood dependency upper bound. Separately, on a supplied finite bipartite split, row-normalized real maps preserve the remote algebraic marginal and Kraus-complete local matrix families preserve the remote partial trace | finite propagation cones and classical or quantum no-signalling | exact fixed-word and algebraic helpers; physical causality attachment not constructed |
Lean/ObserverPatchHolography/Locality/DependencyCone.lean, Lean/ObserverPatchHolography/Locality/NoSignalling.lean |
| For concrete localRepair, a supplied adaptive scheduler and supplied ConsultsOnly consultation region have the exact n-step cone bound ball(S union R,n); a one-site change outside ball(S,n) union ball(R,n) cannot change the probe readout. A two-cell control proves the consultation term is indispensable. Declared refinement maps and one-step intertwining imply cone-image inclusion and run/readback naturality | adaptive finite update locality under an explicitly bounded consultation region | exact conditional helper; source scheduler and physical channel attachment not constructed |
Lean/ObserverPatchHolography/Locality/AdaptiveScheduler.lean |
| A supplied positive normalized exponential tilt on a finite history type obeys the finite information-projection Pythagorean and minimizer identities; inverse-noise mass on all strict nonminimizers tends to zero. Separately, a real local-action minimum under every single-site variation gives the scalar discrete Euler--Lagrange equation and local Noether transport, with a nonzero free-path witness. No finite real-path family contains every such variation. For the committed binary chain, the bilinear corner extension has no velocity solver, while an infinite positive-curvature family agrees on every source history and gives regular strictly convex Lagrangians and Hamiltonians; its checked curvatures one and two are distinct on both faces. Supplied counting-reference and trivial-datum inputs conditionally realize the uniform transition kernel; scale and initial-law controls show this does not select the complete path reference. Two exact multiplier tilts have distinct mean actions, and the matching quadratic gives one unique positive parameter at the supplied empirical target. A concave three-record history is stationary but not minimal and is not a positive-Gibbs mode against one variation, giving only a scoped mode/minimizer control | Gibbs path selection, least-action limits, discrete Euler--Lagrange equations, and Noether currents | exact conditional helpers plus finite/real and real-enrichment non-identifiability boundaries; physical composition is not constructed |
Lean/InformationProjection/PathGibbs.lean, Lean/Variational/DiscreteEulerLagrange.lean, Lean/Variational/DiscreteNoether.lean, Lean/Variational/FiniteHistoryBridge.lean, Lean/Variational/RealizedHistoryLegendreNoGo.lean, Lean/InformationProjection/SourceReferenceSelection.lean, Lean/InformationProjection/SourceHistoryPacket.lean, Lean/InformationProjection/LogTransitionAction.lean, Lean/Variational/StationarySaddleCoverage.lean |
| On the declared unbroken Maxwell action and deconfined phase branch, the quadratic operator has zero hard mass parameter and two transverse classical modes with characteristic surface k^2=0 | massless classical electromagnetic propagation | conditional structural |
code/particles/runs/status/carrier_mode_acceptance.json |
| On the declared pure Yang-Mills quadratic branch before nonperturbative confinement, every color generator has two transverse perturbative modes and zero hard quadratic mass parameter | perturbative color-gauge kernel before confinement | conditional structural |
code/particles/runs/status/carrier_mode_acceptance.json |
| On the declared pure Einstein-Hilbert linearization about a suitable Ricci-flat background, the transverse-traceless quadratic operator has zero hard mass parameter and two classical modes with null characteristic | two massless classical gravitational-wave polarizations | conditional structural |
code/particles/runs/status/carrier_mode_acceptance.json |
| The declared charged-double-triplet current fixture has a direct-sum algebra with adjoint branch dimensions 8, 3, and 1. Its adjoint therefore contains no mixed (3,2,-5/6) (+) (bar3,2,+5/6) X/Y generator, so the ordinary minimal simple-GUT X/Y exchange channel is absent | the Standard Model product adjoint contains no connected simple-GUT X/Y generator | conditional algebraic channel exclusion |
code/a5_closure/receipts/port_current_inner_reference.receipt.json |
| The committed oriented twenty-face incidence has rank 19 and kernel exactly the port gradients. Its local seam Hessian has five nonzero entries per row; gauge invariance and stationary solvability are equivalent to conserved seam current. A separate scalar action has the neutral Green potential as its minimum modulo constants, and the direct-product theorem retains port load and seam current as distinct types | static Maxwell-shaped local curvature and Coulomb sectors | exact conditional finite structural composition |
Lean/Screen/LocalFaceMaxwellAction.lean, code/electromagnetism/runtime/local_face_maxwell_action_receipt.json |
| One explicit (86,88,247) carrier recovers both committed 32-row paths and counted pair states, both checkpoint partitions, and both marginal evolutions over exactly the 31 adjacent source transitions. The pair operator inclusions have full M13 intersection, generate M2366, and intertwine those transitions; admitted operator lifts of source generators retain full generation under the declared transport | common coupling of the two committed correlation packets | exact conditional state/path/checkpoint coupling and finite operator join |
Lean/QFT/TripleCarrierJoin.lean, Lean/QFT/TripleCarrierOperatorJoin.lean, code/source_operator_join/operator_join_packet.json, code/source_operator_join/verify.py |
| One supplied ambient-cofinal spectral family with no terminal regulator and strict finite-carrier growth carries uniform and cofinal-tail concentration. A supplied calibrated-stage energy identification yields exact off-minimum-mass equality and the same envelope; the family also has infinitely many stages and the directly constructed finite four-law core | low-temperature control on a genuine regulator family | exact conditional thermodynamic structure |
Lean/Thermodynamics/CofinalSpectralTailFamily.lean |
| The complete seam symbol has global quadratic consistency error a^2|k|^4/20 and frequency error a^2|k|^3/20. On a supplied common Euclidean domain, its declared reversible curl pair assembles to real L2 fields converging strongly to local Maxwell evolution, uniformly on bounded times, with an O(a^2) H3-to-L2 rate and same-forcing Duhamel bound. Prescribed charge continuity propagates initial Gauss constraints. Lean checks scalar estimates; the L2 assembly and source/limit statements are proved in the paper | Classical continuum Maxwell equations; no measured data | analytic continuum field bridge on a supplied domain and dynamics |
Lean/Screen/SeamMaxwellContinuum.lean, code/electromagnetism/runtime/seam_maxwell_continuum_receipt.json, code/electromagnetism/seam_maxwell_continuum.py, code/electromagnetism/verify_seam_maxwell_continuum.py, paper/screen_microphysics_and_observer_synchronization.tex |
| Exact classical baseline/response feedback restores every pair and every finite overlapping probe word. Serial decoding recovers all 42 typed potential coordinates and preserves electric/magnetic fields and the finite neutral-pair action. Decoded initial records and the charged path current advance a third rational slice | Finite Maxwell field and charged-path equations; no measured data | exact classical software instrument and decoded finite action join |
Lean/Screen/SerialMaxwellReadout.lean, code/electromagnetism/runtime/serial_maxwell_readout_receipt.json, code/electromagnetism/serial_maxwell_readout.py, code/electromagnetism/verify_serial_maxwell_readout.py, paper/observers_are_all_you_need.tex |
| Exact gauge-covariant cone cochain extension preserves decoded boundary fields, Faraday and zero magnetic divergence; closed two-form extension exists exactly at zero total boundary flux. Whitney interpolation supplies piecewise polynomial fields on a declared solid and time slabs. Exact temporal coefficient identities and numerical spatial action/residual controls distinguish the interpolated action from the counting action; all 68 finite-element free-coordinate derivatives are checked for each of two gauge histories | Mathematical Maxwell cochain and variational identities; no observed data | exact finite cochain and coefficient theorems; numerical geometric action/residual audit; no physical postdiction |
Lean/Screen/ConeCochainBridge.lean, Lean/Screen/WhitneyTimeBridge.lean, code/electromagnetism/runtime/cone_whitney_bridge_receipt.json, code/electromagnetism/cone_whitney_bridge.py, code/electromagnetism/verify_cone_whitney_bridge.py, code/electromagnetism/test_cone_whitney_bridge.py, paper/observers_are_all_you_need.tex, paper/tex_fragments/CONE_WHITNEY_BRIDGE.tex |
| Full-metric prism action yields a unique next finite volume potential, preserves the initial Gauss residual under source continuity, and obeys an exact work identity. Positive-mode boundedness has the sharp window 0<h^2 lambda<12; stable initial-value dynamics can have a singular fixed-endpoint problem at h^2 lambda=3. Lean derives the exact Q(sqrt5) Whitney mass forms from the committed supplied coordinates and signed incidence, proves their assembled positivity and K<24M, and supplies the existing stability consumer. Certificate payloads are bound to a kernel witness, while independent numerical quadrature checks the signed assembled forms. A separately Gauss-projected numerical history has two 805-event gauge representatives, all 68 action derivatives verified, exact serial readback restoration and a separately identified 64-slab numerical continuation. | Mathematical classical/quantum field structures; no observed data | exact finite action/stability theorems and algebraic matrix certificate; numerical trajectory and authenticated classical records; no observed postdiction |
Lean/Screen/WhitneyMaxwellDynamics.lean, paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_MAXWELL_DYNAMICS.tex, Lean/Screen/WhitneyFiniteCertificate.lean, Lean/Screen/WhitneyAlgebraicLDL.lean, Lean/Screen/WhitneySourceGeometry.lean, Lean/Screen/WhitneySourceAssembly.lean, Lean/Screen/WhitneyCertifiedConsumers.lean, Lean/Screen/WhitneySourceNaturality.lean, Lean/Screen/WhitneyGeneratedCertificate.lean, Lean/Screen/WhitneyOmittedCellCounterexample.lean, code/electromagnetism/runtime/whitney_maxwell_dynamics_receipt.json, code/electromagnetism/whitney_maxwell_dynamics.py, code/electromagnetism/verify_whitney_maxwell_dynamics.py, code/electromagnetism/test_whitney_maxwell_dynamics.py |
| The same geometric mass/stiffness action has a thirty-dimensional homogeneous transverse sector. Lean derives the concrete positive mass forms from the committed supplied cone geometry and constructs a complete mass-orthonormal positive spectral frame that pulls its source-free continuous-time action back to ordinary oscillators. The derived frame supplies the existing classical-action and polynomial-quantum consumers. Canonical bosonic quantization with supplied positive hbar gives exact polynomial CCR, occupation energies and Heisenberg equations. The paper constructs the factorial-weight Hilbert completion l2(N^30), self-adjoint diagonal Hamiltonian and strongly continuous unitary flow. A separate exact Legendre map identifies the stable prism-step modified oscillator Hamiltonian and a second-order classical temporal limit at fixed bounded spectrum. | Mathematical classical/quantum field structures; no observed data | exact conditional algebraic quantum realization; analytic Hilbert/domain and temporal-limit proof in the paper; no observed postdiction |
Lean/Screen/WhitneyQuantumBridge.lean, paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_MAXWELL_DYNAMICS.tex, Lean/Screen/WhitneyFiniteCertificate.lean, Lean/Screen/WhitneyAlgebraicLDL.lean, Lean/Screen/WhitneySourceGeometry.lean, Lean/Screen/WhitneySourceAssembly.lean, Lean/Screen/WhitneyCertifiedConsumers.lean, Lean/Screen/WhitneySourceNaturality.lean, Lean/Screen/WhitneyGeneratedCertificate.lean, Lean/Screen/WhitneyOmittedCellCounterexample.lean |
| Real Whitney edge integrals dress nodal complex scalar fields by straight-segment U(1) phases, giving exact nodal interpolation, gauge covariance and matching face traces. Restriction of a supplied nonnegative-potential scalar-QED action to these fields and the same volume Maxwell variables gives a joint gauge-invariant action. The paper proves its Noether/Gauss identity, positive temporal-gauge velocity Hessian and global finite-dimensional classical evolution, and constructs nonzero locally charged but globally neutral exact initial data. | Mathematical classical/quantum field structures; no observed data | exact finite interpolation gauge algebra; analytic coupled-action and global-existence proof; no observed postdiction |
Lean/Screen/WhitneyChargedMatter.lean, paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_CHARGED_MATTER.tex, code/electromagnetism/test_whitney_charged_matter.py |
| On conforming shape-regular refinements of the same cone, the supplied dressed scalar/Whitney action and its full real first variation approximate the continuum scalar-electrodynamics action at O(delta), uniformly on bounded piecewise W^{1,infinity}_t W^{2,infinity}_x windows with compatible traces. The analytic proof controls the potential-dependent scalar interpolation and all dressing derivatives. Five finite Lean identities establish cancellation/error algebra; a manufactured-field refinement packet independently checks the implementation on three meshes. | Mathematical classical/quantum field structures; no observed data | analytic smooth-window action/first-variation consistency; finite Lean algebra and numerical refinement checks; no observed postdiction |
Lean/Screen/WhitneySpatialConsistency.lean, paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_SPATIAL_CONSISTENCY.tex, code/electromagnetism/runtime/whitney_spatial_consistency_receipt.json, code/electromagnetism/whitney_spatial_consistency.py, code/electromagnetism/verify_whitney_spatial_consistency.py, code/electromagnetism/test_whitney_spatial_consistency.py |
| For the same interacting finite charged action with nonzero charge, the actual positive kinetic metric gives a smooth Schur metric on the global mean-zero-gauge Coulomb slice R^30 x C^13. Uniform fixed-mesh nodal coercivity gives two-sided polynomial metric bounds and proves that this configuration metric is complete. The declared Laplace--Beltrami operator with nonnegative potential is essentially self-adjoint on compactly supported smooth functions; its unique self-adjoint closure agrees with the Friedrichs realization for the chosen quantization measure and ordering. The residual U(1)-invariant subspace reduces the Hamiltonian and has a dense invariant operator core as well as a form core. An explicit metric-density-corrected Gaussian is exactly normalized, neutral and in the Hamiltonian domain. Independent exact initial-state moment identities provide mathematical observables; no quantum time history is computed. The same reconstructed gauge-invariant scalar quadratic/quartic and magnetic smearings define self-adjoint multiplication operators on maximal neutral domains, a joint spectral PVM and a pushforward probability law for every normalized neutral state. Bounded Borel detector functions retain the identical classical configuration readout. Under the separately stated smooth real Neumann reference and Ritz initialization, scalar smearings and fixed Lipschitz detector responses converge classically at O(1/n). | Mathematical classical/quantum field structures; no observed data | analytic gauge-reduction, metric-completeness and essential-self-adjointness proof; exact normalized initial state and initial observables; no observed postdiction |
paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_INTERACTING_QUANTUM.tex, paper/tex_fragments/WHITNEY_COMMON_OBSERVABLES.tex, paper/tex_fragments/WHITNEY_REAL_CONTINUUM.tex, code/electromagnetism/whitney_interacting_quantum.py, code/electromagnetism/test_whitney_interacting_quantum.py, code/electromagnetism/runtime/whitney_quantum_state_receipt.json, code/electromagnetism/whitney_quantum_state.py, code/electromagnetism/verify_whitney_quantum_state.py, code/electromagnetism/test_whitney_quantum_state.py |
| A five-real-coordinate icosahedrally invariant sector of the same charged action evolves from the nonzero neutral initial data with all 68 full temporal-gauge Euler equations and all 13 Gauss equations checked at 81 samples. The analytic finite-group argument lifts the restricted equations to the full action. The independent verifier reconstructs unrestricted element Jacobians, re-integrates the path and RK4 controls, verifies degree-five quadrature, and rejects omitted-dressing and underintegration controls. Stored classical field readouts include electric cochains, matter fields and local charge. | Mathematical classical/quantum field structures; no observed data | analytic full variational symmetry lift and numerical charged trajectory with independent replay; no observed postdiction |
paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_CHARGED_EXECUTION.tex, code/electromagnetism/runtime/whitney_charged_dynamics_receipt.json, code/electromagnetism/whitney_charged_dynamics.py, code/electromagnetism/verify_whitney_charged_dynamics.py, code/electromagnetism/test_whitney_charged_dynamics.py |
| A conforming uniformly shape-regular refinement of the same solid supports the full charged action's invariant real scalar sector with A=phi=0. Given a C^2([0,T];H^2) real Neumann solution and mass-shifted Ritz initial position and velocity, the semidiscrete nonlinear wave trajectories converge at O(1/n) in H^1 position plus L^2 velocity, uniformly on the fixed time interval. The proof uses the actual invariant sector and retains its full-action equations and constraints. | Mathematical field, software-instrument and quantum structures; no observed data | analytic conditional real-sector continuum trajectory bound; independent finite geometry/Ritz and wave checks; no observed postdiction |
paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_REAL_CONTINUUM.tex, code/electromagnetism/runtime/whitney_real_continuum_receipt.json, code/electromagnetism/whitney_real_continuum.py, code/electromagnetism/verify_whitney_real_continuum.py, code/electromagnetism/test_whitney_real_continuum.py |
| Five computational observer-like patches execute 1782 events with local coordinate/velocity states, ring ports, destructive averaging probes, retained records and feedback. All 405 probe cycles restore their rational registers exactly. Eighty numerical action advances consume decoded states; 81 decoded frames reconstruct the same charged action's full fields, with all 68 configuration equations and 13 Gauss equations independently checked. A separate exact consumer freshly verifies the charged IVP enclosure and record replay: all ten decoded q/v coordinates at nominal j/40 checkpoints lie within 10001/10^14 of the exact trajectory. Historical samples remain comparison-only inputs, not instrument evolution inputs. | Mathematical field, software-instrument and quantum structures; no observed data | exact software readback/restoration, replayed numerical fields and separately certified decoded checkpoint errors; no observed postdiction |
paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_CHARGED_INSTRUMENT.tex, code/electromagnetism/runtime/whitney_charged_instrument_receipt.json, code/electromagnetism/whitney_charged_instrument.py, code/electromagnetism/verify_whitney_charged_instrument.py, code/electromagnetism/test_whitney_charged_instrument.py, code/electromagnetism/runtime/whitney_charged_checkpoint_receipt.json, code/electromagnetism/whitney_charged_checkpoint.py, code/electromagnetism/verify_whitney_charged_checkpoint.py, code/electromagnetism/test_whitney_charged_checkpoint.py |
| The complete coupled kinetic metric, potential and supplied energy define the Jacobi-Maupertuis duration d_tau=sqrt(G[dq,dq]/(2(E-V))). On a regular nonturning stationary path of the fixed-energy Jacobi action, this timing recovers the natural action evolution and is invariant under positive reparameterization. A consumer integrates polygonal paths through 81 independently decoded configurations without using recorded velocities, timestamps or repair counts in its clock integral. A fixed smooth nonturning curve has an analytic O(delta^2) polygon-duration estimate. | Mathematical field, software-instrument and quantum structures; no observed data | standard Jacobi timing attached to the same action and software records; independently replayed numerical readout; no observed postdiction |
paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_EPHEMERIS_CLOCK.tex, code/electromagnetism/runtime/whitney_ephemeris_clock_receipt.json, code/electromagnetism/whitney_ephemeris_clock.py, code/electromagnetism/verify_whitney_ephemeris_clock.py, code/electromagnetism/test_whitney_ephemeris_clock.py |
| The full 56-real-coordinate interacting Hilbert space admits the explicitly time-dependent neutral trial v(t)=exp(-itV/hbar)f_sigma. Exact global Gaussian moments and analytic coefficient bounds certify its Hilbert-norm distance from the exact Hamiltonian evolution for every time in a declared short interval. The packet supplies five times and four exact phase configurations while keeping the configuration probability density fixed; it does not restrict the quantum state to the classical five-coordinate trajectory. | Mathematical field, software-instrument and quantum structures; no observed data | analytic trial-evolution error theorem and independently replayed exact global bound; no observed postdiction |
paper/observers_are_all_you_need.tex, paper/tex_fragments/WHITNEY_QUANTUM_HISTORY.tex, code/electromagnetism/runtime/whitney_quantum_history_receipt.json, code/electromagnetism/whitney_quantum_history.py, code/electromagnetism/verify_whitney_quantum_history.py, code/electromagnetism/test_whitney_quantum_history.py |
| A supplied spin lift and conserved single-occupation current histories do not select exchange statistics. A separate same-channel two-particle comparison has exact coincidence probabilities 1, 49/625 and 337/625 for the declared fermionic, bosonic and distinguishable preparations. | Pauli exclusion (target only; no physical comparison) | conditional statistics-identification boundary and exact finite comparison |
paper/tex_fragments/SPIN_EXCHANGE_SELECTION_BOUNDARY.tex, code/spin_exchange/receipt.json, code/spin_exchange/verify.py |
| A common real scalar-q creation law and exact quadratic occupation/phase law force q in {1,-1}. Finite full representation dimension, or a stable fixed negative-energy ladder, excludes q=1 and yields Pauli exclusion and full canonical anticommutation by polarization. | Pauli exclusion (target only; no physical comparison) | analytic conditional exclusion with independently checked finite controls |
paper/tex_fragments/PAULI_STABILITY_SELECTION.tex, code/pauli_stability/receipt.json, code/pauli_stability/verify.py |
| On a finite positive Hilbert space, an unscaled contraction creation field with its exact quadratic unit-phase law squares to zero. Linearity gives creation anticommutation without a scalar-q premise. An exhaustive adjoint add/remove instrument additionally yields full CAR. A covariant symmetric Fock space capped at total occupation two preserves the supplied one-particle source dynamics and exact phase law but permits double occupation. Making its fields into Kraus contractions rescales the quadratic phase law. | Pauli exclusion (target only; no physical comparison) | analytic conditional operation theorem and exact source-bound countercontrols |
paper/tex_fragments/PAULI_SOURCE_SELECTION_BOUNDARY.tex, code/pauli_source_selection/receipt.json, code/pauli_source_selection/verify.py |
Lean declaration bindings:
gauge_lie_algebra:A2HolonomyBridge:internalImplementation_of_holonomy,four_factor_fixed_dimension_ne_one,compact_product_dimensions_of_fixed_space;A5OPH:sum_eq_eleven,sum_eq_twelve,action_trivial_of_card_le_four,sum_not_mem_excluded,quintet_noncentral;A5CharacterField:multiplicities_equal_of_galoisStable,centreDim_mem_trichotomy_list;A5SixAxes:two_transitive,V5_irreducible,no_three_plus_three_splitoriented_face_nearest_compact_discriminator:OrientedFaceBracketSelector:face_bracket_eq_sixty_r13,jacobi_failure_witness,unique_nearest_G,three_norm_unique_nearest_Ginvariant_metric_phase_diagram:OrientedFaceInvariantMetric:reference_G,dG2_lt_dP2,dF2_lt_dP2,balanced_unique_nearest_G,box_unique_nearest_G,F_wins_at_witnessgauge_kinetic_invariant_form_drop:GaugeKineticInvariantForms:f_exact_two_parameter,g_exact_two_parameter,p_exact_two_parameter,mirror_common_extra_premise_one_raytwo_factor_constructed_history_binding:TwoFactorHistoryBinding:twoFactor_kernel_identifies_weighted_coefficients,twoFactor_kernel_only_common_multiplier_scaling,fullP_action_reproduces_law,fullP_kernel_relative_coefficients_identifiable,fFamily_action_reproduces_law,fFamily_kernel_relative_coefficients_identifiableglobal_form_z6:Z6Exact:gauge_eq_kernel,residue_surjective,representative_formula;Z6Descent:kernel_on_realized_weights,four_admissible_global_forms,sixAxis_generator_maps_to_kernel_generator,sixAxisToKernel_intertwines_involutions,sixAxisToKernel_injective,sixAxisToKernel_rangehypercharge_spectrum:ExteriorSelection:selection_unique,parity_sectors_survive,conj_exchanges_survivors,witten_automatic;WeylYukawaConventions:conjugate_charge_dictionary,weyl_up_neutral,weyl_down_neutral,weyl_lepton_neutral,dirac_up_neutral,dirac_down_neutral,dirac_lepton_neutral,mixed_convention_not_neutralfinite_quantum_limitation_suite:Robertson:finite_state_robertson_commutator,neg_I_mul_commutator_expectation_eq_readout,pauliX_pauliY_ne_pauliY_pauliX,pauli_xy_noncommuting_control,pauliZ_pauliX_ne_pauliX_pauliZ,pauli_z_zero_variance_control;Superselection:partitionOperationallyEquivalent_iff_pinching_eq,trace_mul_eq_zero_of_partitionOffDiagonal,partitionPinching_partitionCorner_eq_zero,partitionAverage_partitionCorner_eq_zero,trace_partitionCorner_mul_eq_zero_of_mem_span;B10EdgeCenterAction:partitionCenterAdaptor_after_blockReadout,partitionCenterAdaptor_surjective,partitionCenterAdaptor_commutes_with_block,rankTwo_pinching_ne_average;RecordMajorization:recordSignAverage_eq_partitionPinching,globalSignAverage_not_binary_pinching;SpectralEntropyBoundary:binary_orthogonal_density_receipt,totalizedRelativeEntropy_binary_orthogonal_eq_zero,supportAware_not_totalizedRelativeEntropymodal_maxwell_factorization_boundary:ModalMaxwellFactorizationBoundary:modalCurlScale_sq_mul_dot_self,dot_modalCurl_zero,modalCurl_sq_on_transverse,complexMomentumDot_fourierCurl_zero,complexPhotonSpatialAction_complexifies,fourierCurl_sq_on_transverse,maxwellShapedModalGenerator_sq_wave,maxwellShapedModalGenerator_transverse,sameSignCurlMutation_sq_positive,sameSignCurlMutation_fails_wavefinite_unitary_scattering_limit_no_go:FiniteUnitaryScatteringNoGo:tendsto_powers_forces_identity,nontrivial_powers_have_no_limit,finite_unitary_powers_have_no_limit,finite_unitary_ambient_powers_have_no_limit,identical_relative_evolution_is_constant,identical_relative_evolution_tendstofinite_exterior_component_bridge:ExteriorComponentBridge:exterior_basis_label_count,bidegree_count_table,componentDegree_exact_nontrivial_menu,component_dimension_binding,component_charge_binding,component_parity_binding,component_conjugation_binding,creation_square_zero,creation_actions_anticommute;QuantumMatterIntegration:even_component_weights_eq_matterWeights,kernel_on_exterior_component_weights,fractional_singlet_mutation_collapses_component_kernel,coordinate_diagonal_not_partitionOffDiagonal,coordinate_nonzero_offDiagonal_control,declaredBlockReadout_eq_iff_operationallyEquivalent,kernel_on_mapped_component_weights,bridge_selection_is_parity_sector;B10EdgeCenterAction:mappedCentralAction_zero,mappedCentralAction_add,mappedCentralAction_neg_comp,mappedCentralAction_eq_id_iff_component_phases_zero,mappedCentralAction_eq_id_iff,mappedCentralAction_kernel_card,selectedMappedMatter_support_is_parity,selectedMappedMatter_nontrivial,mappedCentralAction_preserves_selected,kernel_on_selected_mapped_components,selectedMappedCentralAction_eq_id_iff,no_selected_central_parameter_realizes_parity_signcoupling_universality:A5CouplingSymmetry:groupAverage_port_independent,coupling_ratio_universal;A5PortAction:transitive_on_ports;PortFrameGram:degree_five,gram_sqintrinsic_rank_three_response_completion:PortGramRepairBand:portGram_unique_lowest_positive_galois_maximal,selected_family_band_is_port_gram;PortGramRepairCovariance:normalizedKernel_tendsto_portGram,portGram_antipodal_quotient;PrimitivePortFrameQuotient:frameQuotient_finrank,quotientEquivVec3_preserves_gram,pointEuclideanFrame_denseRange;RepairWordCarrierReadout:loadPosition_denseRange,universalPosition_isometry;SeamCurrentCarrierQuotient:exists_seamCurrent_iff_even,d6Position_denseRange,d6Position_isometry;PortGramA5Isometry:selected_band_action_faithful,carrierRotation_isometrylayered_discrete_gauss_boundary:LayeredDiscreteGauss:sum_vertexOutflow_eq_regionFlux,steady_total_source_eq_zero,unbounded_shellCard_forces_zero,regionFlux_eq_charge,shell_total_eq_charge,perEdgeFlux_eq,scale_free,chainWitness_charge,regionFlux_twelvePort,steady_witness_regionFlux_eq_sourcecarrier_class_dispersion_band:A5CarrierClassBand:band_endpoints,tuned_zero,gap_zero_iff_single_radius,general_member_in_band,cross_order_lock,cross_order_polynomial,multi_radius_negative_controlpositive_cosine_frequency_contraction:CarrierFrequencySpeed:feature_norm_sq_eq_cosineSymbol,feature_dist_le,frequency_global_one_lipschitz,edge30_cosineSymbol_eq_fz12,fz12_frequency_global_one_lipschitz,unit_port_second_moment_eq,vertex12_cosineSymbol_eq_fz11,fz11_frequency_global_one_lipschitztime_order_type_ledger:TimeOrderLedger:canonicalLedgerKinds_pairwise,offsetGauge_nebounded_observer_time_calibration:ObserverHistory:threeRecord_control,discreteConstantClock_not_injective;ClockReadout:cubicThreeTickClock_not_affine,throughTwoPoints_unique;WorldlineRealization:displacement_futureTimelike_in_chart,threeRecord_twoChart_futureTimelike;ProperTimeCalibration:properTimeBetween_sq_eq_interval_in_chart,properTimeBetween_add;ClockComparison:onePoint_not_unique,calibration_unique,affineConsistent_iff_crossMultiplicationfinite_public_record_algebra_and_sharp_no_cloning:PublicRecordAlgebra:publicSubalgebra_mul_comm,publicSubalgebra_le_commutant,recordSynthesisStarAlgHom_bijective,publicRecordFunctionEquiv_apply;NoBroadcastingAdapter:SharpCloneWitness.overlap_zero_or_one,SharpCloneWitness.eq_of_overlap_one,SharpCloneWitness.orthogonal_of_ne,NoBroadcastingAdapter.objective_pair_compatiblefinite_consensus_tower_interface:ConsensusTower:public_mem_refine,refine_recordElement,refine_precedes,refine_generator,refine_state_pairing,constantConsensusTower_public,constantConsensusTower_recordElementfinite_public_world_endpoint:PublicWorldQuotient:toPublicWorld_eq_iff,publicSignature_injective,hiddenBit_distinct_but_publicly_equal;FixedPointEndpoint:public_endpoint_exists_unique_on_public_class,publicRepair_idempotent,lr_public_endpoint_exists_unique_on_gauge_class,representative_no_descended_repair,primitiveLR_endpoint_exists_unique_on_gauge_classcanonical_intrinsic_lorentz_module:CanonicalLorentzModule:det_toMatrix,isHermitian_iff_existsUnique_toMatrix,finrank_Herm2,time_axis_positive,spatial_axis_negative;CelestialNullCone:rayToCelestial_celestialToRay,celestialToRay_rayToCelestial;ObserverFrameHyperboloid:frame_time_sq_eq_one_add_spatial,frame_time_ge_one;ObserverRestSpace:finrank_restSpace,restMetric_pos,restMetric_self_eq_zero_iff;EinsteinTensorBridge:lorentzQ_eq_neg_einsteinQuad,lorentzQ_eq_zero_iff_einsteinQuad_eq_zero,isFutureNull_iff_einsteinsource_derived_finite_one_three_causal_carrier:CausalInterval:finiteCausalSetAxioms;SemanticEventProvenance:sourceHeight_eq;SourceDerivedSpacetimeCarrier:sourceSpacetimeCarrier_finrank,sourceCarrier_one_three_signature,sourceUnitNullVector_futureCausal,generatedBefore_sourceCausalLE,generatedBeforeEq_iff_sourceCausalLE,exactDiamondConeOrder;SourceOrderFrameCompatibilityPacket:SourceOrderFrameCompatibilityPacket.ofFaithfulPlacement,SourceOrderFrameCompatibilityPacket.ofFaithfulPlacementStandardFrame,sourceOrderFramePacket_consequencesalgebraic_event_frame_soldering:LorentzOverlapCocycle:LorentzOverlapCocycle.act_cocycle,LorentzOverlapCocycle.act_reverse_left,LorentzOverlapCocycle.act_reverse_right,LorentzOverlapCocycle.act_sub_act;EventGermDisplacement:coincidenceInvariant_iff_existsUnique_descendedReadback,overlapControl_not_transitive,EventGermAtlas.displacement_reverse,EventGermAtlas.displacement_chain,EventGermAtlas.displacement_overlap,EventGermAtlas.interval_overlap;CelestialSoldering:OrientedLorentzEquiv.mapFutureNullRay_trans,OrientedLorentzEquiv.celestialAction_trans,EventGermAtlas.futureNullDisplacementRay_overlap,EventGermAtlas.celestialSolder_overlap;EventFrameSoldering:EventFrameSoldering.algebraicConsequences,control_chart_translation_nonzero,control_displacement_nonzero,control_displacement_futureNull;SpatialReadbackSoldering:restProjection_decomposition,OrientedLorentzEquiv.restProjection_covariant,OrientedLorentzEquiv.restEquiv_preserves_metric,frameQuotientEquivStandardRest_preserves_metric,EventFrameSoldering.displacement_time_add_spatial,EventFrameSoldering.spatialReadback_overlapfinite_causal_observer_net_interface:FiniteCausalObserverNet:commute_of_disjoint,regionalExpectation_refine,relaxedRepair_compose,relaxedRepair_fixes_disjoint,relaxedRepair_remote_expectation,kraus_remote_marginal_invariant,fullM2_distinct_regions_not_local,idempotence_does_not_force_remote_fix,partitionPublicCausalNet_has_disjoint_pair;ObserverNetDescent:jointly_injective_of_unique_descent,no_descent_of_indistinguishable_global_sections,glue_restrict,glue_unique,partitionPublicTwoRegionCover_hasUniqueDescent;RichFibreWitness:richSupport_pairwise_disjoint,richSplit_census;RichFibreRegionalNet:richRegional_noncommutative_all,richDesignatedFactor,richWindowCover_coverageLaw,richDropCover_not_coverageLaw,richWindowCover_reconstruction;SourceOperatorGeneration:sourceAlgebra_eq_top,obs86_sourceAlgebra_eq_top,obs88_sourceAlgebra_eq_top,obs247_sourceAlgebra_eq_top,obs384_sourceAlgebra_eq_top,obs86_projectors_only_ne_top;JointSlotFactorisation:obs86_lifted_eq_leftSlot,obs88_lifted_eq_rightSlot,slot_commute,obs86_checkpoint_pinch_no_signalling,rightSlotExpectation_fixes_right,rightSlotExpectation_posSemidef;CPRestrictionNet:restrictCP_comp,slot_ranges_generate_top,no_scalar_restriction_of_matrix_factor;TwoSlotCPNetWitness:slotExpectations_not_jointly_injective,checkpoint_pinch_fixes_right,twoSlot_left_no_scalar_hom;TowerAnchoredDiamond:anchoredTower_privateAlgebra,partition_members_in_left_region,anchoredCheckpointPartition_proper,anchoredNet_left_ne_top;SourceCorrelationCapstone:supports_disjoint,slotExpectations_erase_source_correlation;StructuralNetAdequacySurface:supportDisjoint_correlation_counted_state,supportDisjointNet_expect_recovers_marginals,supportDisjoint_composed_adequacy,supportDisjoint_swap_covariancefinite_publicization_dynamics:PartitionAverageCP:ProjectivePartition.partitionAverageKraus_complete,partitionAverage_kraus_form;TwoScalePublicRepair:publicRelax_compose,publicRelaxTime_add,publicRelaxTime_residual;PoissonizedRepair:poissonizedRepair_add,repairGenerator_eq_zero_iff,hasDerivAt_poissonizedRepair_eq_generator;PoissonizedRepairOperatorExp:normedSpace_exp_smul_idempotent,normedSpace_exp_continuousRepairGenerator,normedSpace_exp_continuousRepairGenerator_apply;ConditionalExpectationGenerator:conditionalExpectationGenerator_eq_projectorGKSL,conditionalExpectationGenerator_eq_zero_iff_mem_commutant,multiCollarGenerator_eq_zero_iff_stableIntersection;ChoiCPTP:partitionAverage_isCPTP,partitionPinching_isCPTP,relaxationChannel_isCPTP,transposeMap_positive_tracePreserving_not_CPfinite_public_private_dynamics:PublicMarkov:recordMapOfKernel_injective,positive_unital_iff_stochastic,activeRecord_positive_unital_iff_stochastic,toPerm_eq_refl,function_action_eq;PublicAutomorphism:publicStarAutomorphism_is_labelPermutation,publicStarAutomorphism_labelPermutation_unique,toAut_eq_refl;PrivateInner:finitePrivateStarAutomorphism_inner,hasDerivAt_realVonNeumannFlow,hamiltonianPropagator_mem_unitaryfinite_holonomy_character_phase:HolonomyInterference:transportRatio_eq_closedLoopHolonomy,relativeCharacterPhase_eq_closedLoopPhase,holonomy_rechart_conjugate,holonomy_rechart_invariant,characterPhase_rechart_invariant,exists_localTriangleFlat_globalHolonomy_nontrivial,long_reference_relativeCharacterPhase,exists_localTriangleFlat_relativeCharacterPhase_nontrivial,zmodCharacter_phase_pow_order,cyclicSectorCharacter_phase_pow_order,loopCharacterPhase_pow_order_of_cyclicHolonomy,cyclicLoopPhase_pow_orderfixed_regulator_operational_overlap_evidence:OperationalOverlapEvidence:operationalObservers_share_visible_event_record,operationalOverlap_good_evidence,operationalOverlap_good_common_mem_both,operationalOverlap_bad_not_evidencefinite_born_frame_rank_gap:FiniteBornFrame:contextAdditive_unique_parameterization,exists_frameCentered_iff_frameRelations,hermitianRepresentation_unique,densityRepresentation_unique,exists_admissible_not_densityRepresentable;FiniteEffectClosureBoundary:continuous_celestialBinaryWeight,nonlinearBinaryWeight_mem_Icc,nonlinearBinaryWeight_antipodal_sum,nonlinearBinaryWeight_not_affine,dense_affine_probability_tests_force_closed_unit_ball;FiniteWebBornNoGo:planarCubicAssignment_noncontextual,finiteBuschGleasonInterface_false,current_finite_web_born_no_go;SourceContextTomographyNoGo:current_source_context_web_not_tomographically_complete,pauliY_context_distinguishes_states;SourcePhaseLiftBridge:sourcePhaseLift_eq_rhoYPlus,sourcePhaseLift_mem_complexSourceAlgebra,realSourceEffectClosure_not_tomographically_complete,sourcePhaseTomography_injective_on_equalTrace,sourcePhaseLift_boundary_summary;ConjugationGauge:bornWeight_re_matrixConj,conj_invisible_on_fixed_effects,yStates_are_conj_orbit;RepairCurrentOrientation:designatedPair_lexLeast,designatedCycle_lexLeast,designatedCycle_normalized_products,reversal_flips_orientation,reversibleControl_no_orientation;SourceOrientedCompletion:orientationApplicable_holds,reversal_selects_conjugate,completionTomography_injective_on_states,oriented_born_capstonethermodynamic_four_law_package:FiniteConditionalRepair:gibbs_pythagorean,gibbs_minimizer,heatBath_row_optimal,heatBath_secondLaw,heatBath_detailedBalance,heatBath_fixes_fiberObservable,kl_push_le,excitedMass_le,excitedMass_lt_of_beta_large,gibbs_beta_injective,clausius,landauer,heatBath_preserves_pos,mixture_stochastic,mixture_stationary,block_entropy_le;StationaryRealization:stationary_secondLaw,constantObservable_fixed,directedLazy3_stationary,directedLazy3_not_detailedBalance,directedLazy3_secondLaw;FirstLawIdentity:firstLaw_split;FluctuationTheorems:integral_fluctuation,crooks_pointwise,crooks_level_set,sigma_mean_eq_kl_descent,correlation_symm,heatBath_integral_fluctuation,heatBath_crooks,heatBath_correlation_symm;CapFirstLaw:cap_firstLaw_exact,cap_firstLaw_split,cap_clausius_of_central_conserved,push_heatBath_fixes_mean,heatBath_cap_clausius;EinsteinPremiseLink:shannon_diff_eq_pairing_sub_kl,thermoFirstLawData_passes,thermo_first_law_on_simplex_tangent,repair_variation_mem_massZero,repair_variation_central_pairing_zero;PartitionPinchingCP:ProjectivePartition.kraus_complete,partitionPinching_kraus_form;ChoiCPTP:partitionPinching_isCPTP;CommonReferenceObstruction:mixingMode_eigenpair,no_nondegenerate_current_common_object_intertwiner,no_empirical_deterministic_stationary_pushforward,current_common_reference_obstruction_summaryfinite_green_kubo_graph_transport:GreenKubo:dissipation_eq_dirichlet,greenKuboPair_symm_of_poisson,greenKuboPair_finite_matrix_psd,greenKuboPair_eq_integratedCorrelation_add_remainder,heatBath_integratedCorrelation_not_stable,heatBath_integratedCorrelation_eq_equalTime,binary_heatBath_integratedCorrelation_eq_one,identityKernel_no_poisson_of_ne_zero;GraphDiffusion:summation_by_parts,fickParticleAmountStep_bridge,fickParticleAmountStep_total_conservation,fourierEnergyStep_bridge,fourierEnergyStep_total_conservation,fick_flux_gradient_power_nonpositive,fourier_flux_gradient_power_nonpositive,negative_conductance_counterexample,negative_thermal_conductance_counterexample,twoVertex_fick_closed_step,twoVertex_fourier_closed_stepfinite_conservation_ward_precursor:RegionalContinuity:regional_continuity,global_continuity,global_conservation_of_zero_total_source,FiniteContinuityWitness.regionalBalance;DiscreteGauss:gauss_solution_exists_iff_total_zero,rationalBoundarySection_is_gauss_solution,gauss_solution_iff_difference_is_cycle,gauss_cycle_space_finrank;ProtectedCharge:chargeExpectation_preserved_iff_dual_fixed,kernel_chargeExpectation_preserved_iff_pull_fixed,twoStateOddCharge_ne_zero,channel_covariance_does_not_imply_charge_conservation;WardLimitManifest:WardLimitManifest.wardIdentityfinite_fixed_word_locality_and_marginal_invariance:DependencyCone:localRepair_agree,applyWord_agree_on,no_influence_outside_ball;NoSignalling:sndMarginal_pushJoint_liftFst,remote_mass_changes_without_row_normalization,ptraceFst_local_krausconditional_adaptive_scheduler_locality_helper:AdaptiveScheduler:adaptiveRun_agree_on,adaptive_no_influence,consultation_region_not_droppable,ball_image,run_natural,readback_cone_boundfinite_history_variational_helpers_and_bridge_obstruction:PathGibbs:pathGibbs_pythagorean,pathGibbs_minimizer,modal_path_least_action,noiseFamily_above_gap_mass_tendsto_zero,noiseFamily_nonminimal_mass_tendsto_zero;DiscreteEulerLagrange:stationary_localAction_discreteEulerLagrange;DiscreteNoether:noether_conserved,noether_current_constant_on_finite_chain,free_translation_nonzero_noether_witness;FiniteHistoryBridge:exists_real_site_variation_outside,not_all_real_site_variations_mem;RealizedHistoryLegendreNoGo:chainLogLagrangian_no_velocity_solver,chainCurvedLagrangian_realized_indistinguishable,chainCurvedLagrangian_one_two_midpoint_gap,chainCurved_legendreTransform,realizedHistory_legendre_nonidentifiability_receipt;SourceReferenceSelection:heatBath_counting_trivial_eq_uniform,reference_realized_under_counting_trivial_inputs,nontrivial_datum_not_invariant,noncounting_reference_not_invariant,heatBath_scaledCounting_trivial_eq_uniform,uniform_transition_does_not_determine_path_reference,committed_tilts_have_distinct_mean_actions;SourceHistoryPacket:sourceMatchQuad_strictMonoOn_pos,sourcePositiveMeanMatch_unique,sourceMatchingPositiveParameter_existsUnique;LogTransitionAction:bare_log_action_multiplier_unique_of_nonconstant;StationarySaddleCoverage:stationaryMaximumHistory_stationary,stationaryMaximumHistory_not_minimal,gibbs_prefers_nonstationarylocal_face_maxwell_static_composition:LocalFaceMaxwellAction:face_port_incidence_product_zero,ker_faceCurvature_eq_gradient,localKineticZ_five_per_row,localSourcedAction_gauge_invariant_iff,localStationary_solvable_iff,greenPotential_stationary,staticAction_global_minimumtriple_observer_carrier_coupling:TripleCarrierJoin:triplePath_projects_88,triplePath_projects_247,tripleCorrelationState_marginal_88,tripleCorrelationState_marginal_247,tripleCheckpoint_recovers_anchored_88,tripleCheckpoint_recovers_anchored_247,tripleMarginals_not_jointly_injective,tripleCarrier_join_receipt;TripleCarrierOperatorJoin:operatorJoin88_injective,operatorJoin247_injective,operatorJoin86_injective,operatorJoin_hinge,operatorJoin_intersection,operatorJoin_generate_top,operatorJoin_spectator_locality,operatorJoin_hinge_noncommuting,operatorJoin88_retraction,operatorJoin247_retraction,operatorJoin88_counted_readout,operatorJoin247_counted_readout,operatorJoin88_evolve,operatorJoin247_evolve,operatorJoinSource88_generates,operatorJoinSource247_generates,operatorJoinAdmitted_generates,operatorJoinAdmitted_evolvedcofinal_spectral_tail_four_law_composition:CofinalSpectralTailFamily:cofinal_tail_concentration,cofinalLadder_card_unbounded,constantCarrier_cofinalFamily_isEmpty,uniformGap_cofinalFamily_isEmpty,fourLaws_composed_cofinalseam_maxwell_continuum:SeamMaxwellContinuum:cosine_quartic_upper,unit_seam_fourth_moment_eq,exact_symbol_quadratic_error,exact_frequency_error,cosine_propagator_error,sine_propagator_errorserial_maxwell_readout:SerialMaxwellReadout:cycle_restores,serial_restores,response_after_prefix,decode_serial,feedback_error,decoded_fields,decoded_coupled_action,decoded_joint_field_stationarycone_whitney_bridge:ConeCochainBridge:extendOne_gradient,extendOne_gauge_covariant,coneCurl_extendOne,coneCurl_gauge_invariant,coneCurl_boundary_trace,extended_curvature_closed,extendTwo_curvature,extendTwo_closed,extendTwo_radial_unique,closed_extension_iff_zero_flux,constant_unit_flux_has_no_closed_extension,zero_apex_constant_gauge_fails;WhitneyTimeBridge:affine_quadratic_polynomial,magnetic_window_action_defect,magnetic_defect_divided_difference,polarized_trapezoid_defect,polarized_defect_divided_difference,temporal_hat_mean,temporal_hat_residual,ampere_covector_decomposition,scalar_nonzero_residual_controlwhitney_maxwell_dynamics:WhitneyMaxwellDynamics:two_slab_action_expansion,scalar_potential_action_expansion,temporal_gauge_ampere_iff_recurrence,recurrence_next_unique,gauss_residual_preserved,pairEnergy_work,modal_solution_bound,criticalMode_unbounded_difference,supercritical_unbounded_solution,two_slab_endpoint_resonancewhitney_radiative_quantum:WhitneyQuantumBridge:reconstruct_surjective,same_action_normal_modes,annihilation_creation,canonical_position_momentum,same_modes_quantized_energy,quantumHamiltonian_monomial,quantumHamiltonian_position,quantumHamiltonian_momentumwhitney_charged_matter:WhitneyChargedMatter:pathPhase_gauge,interpolate_gauge,interpolate_gauge_norm,interpolate_vertex,interpolate_face_tracewhitney_spatial_consistency:WhitneySpatialConsistency:weighted_antisymmetric_cancellation,weighted_path_phase_zero,polarized_cancellation,centered_dressing_error,centered_potential_variation
Hypothesis boundaries:
gauge_lie_algebra: the abstract theorem uses the A1 faithful complete compact response and A2 endogenous holonomy clauses. The direct receipt verifies a declared charged-double-triplet witness and does not reconstruct it from ordered source histories or identify a laboratory current. Compact reductivity and the compact-simple classification are declared classical inputsoriented_face_nearest_compact_discriminator: the equal-weight oriented-face construction is a declared deterministic rule applied to the pinned incidence orientation, not a rule forced by the OPH axioms. The comparison adds three basis-dependent coordinate norms; neither a norm, minimum-distance repair, nor any Jacobi-repair dynamics is source-derived. Exact code proves the 792-coordinate optimization, while Lean checks the serialized radical values and order. The result compares only with the classified compact locus and does not close B14 or select a physical gauge bracketinvariant_metric_phase_diagram: the closed forms are certificate content derived from the pinned tensors by the independently replayed producer; Lean proves the phase consequences as quantified real theorems over those forms. The nearest-point repair rule and the restriction to carrier-induced metrics are declared discriminator choices, the comparison is conditional on the classified compact locus, and no metric, bracket, current, or physical gauge structure is source-selectedgauge_kinetic_invariant_form_drop: the brackets and carrier projectors are supplied certified finite objects. The theorem selects neither bracket nor overall or relative coupling coefficients, and it constructs no source action, continuum field, or laboratory current. The one-ray intersection cannot be promoted without the additional simultaneous-invariance premisetwo_factor_constructed_history_binding: both transition kernels are Gibbs kernels constructed from the displayed two-factor costs. The theorem symbolically handles the 729- and 177147-state groups without a large enumeration. It does not identify either kernel with an independently source-produced process, select either coefficient or their ratio, add the abelian sector, or supply physical units, a continuum field, laboratory current, or predictionglobal_form_z6: the result is exact for the declared matter table, central descent congruence, axis coefficient relations, and line lattice. The source current, physical matter action, relation-lattice selection, character completeness, loop-to-kernel identity, laboratory attachment, and continuum quantum field theory remain outside this resulthypercharge_spectrum: the selection is exhaustive inside the declared exterior algebra; completeness beyond that algebra, selection of one charge-conjugate representative, light-sector attachment, family multiplicity, scalar content, and laboratory identification remain separatefinite_quantum_limitation_suite: the state, observables, and projective partition are supplied finite inputs. Pinching lands in the generally noncommutative commutant, while averaging lands in the commutative projector span. The adaptor is relative to that supplied partition. The sign average is an exact precursor, not a proof of spectral majorization. The totalized-log countermodel rejects only that naive architecture; a support-aware extended divergence, pinching Pythagoras, constrained maximum entropy, and the publicization information chain are not constructed. Scientific owner #730 records those quantum-composition obligations; #739 records any residual premise-discharge obligation. No source rule selects that partition, a state, an observable, a detector algebra, or a public instrument, and no edge-to-partition identification is constructedmodal_maxwell_factorization_boundary: this is a pointwise Fourier-modal/pseudodifferential factorization of a committed mathematical oscillator. Its momentum-dependent multiplier supplies no local position-space operator, real-field assembly or opposite-momentum reality pairing, electric/magnetic identification, source-produced dynamics, U(1) potential or gauge quotient, Maxwell action, bridge from the finite Gauss receipts to this modal divergence, conserved physical current or source coupling, Lorentz covariance, continuum control, or laboratory readout. It removes no registered premise: PR-20, PR-21, and PR-22 remain declared inputs, while PR-53 and PR-54 name missing attachments. Scientific owner #733 records those obligations. This row emits no frozen predictionfinite_unitary_scattering_limit_no_go: this is only a no-go for direct ordinary convergence of one fixed-cutoff power sequence U^n. Full weak-operator convergence at that same finite dimension is excluded too, because the standard finite-dimensional operator topologies coincide. It leaves relative or comparison dynamics, selected projected scalar or observable limits, infinite-dimensional weak limits, subsequential or Cesaro limits, continuum or infinite-volume limits, open-system evolution, and finite-time operational protocols unresolved by this result. It constructs no wave operator, S-matrix, cross section, pole, optical theorem, renormalization flow, or continuum QFT. Scientific owner #743 records those interacting-QFT, renormalization, and scattering obligations. This row emits no frozen predictionfinite_exterior_component_bridge: the exterior carrier, component-to-sector map, central-weight labels, and separate selection mask are supplied finite inputs. The character action is imposed through those weights rather than derived from ambient-projector conjugation, and projector ranks are not bound to exterior multiplicities. The universal minus-one result is only a nonconflation control and constructs no physical fermion parity. No source rule selects a physical matter action, and the package proves no continuum spin-statistics, particle spectrum, physical global form, or laboratory chargecoupling_universality: reduces the universality clause to A5-equivariance of the implemented source law; no coupling value is impliedintrinsic_rank_three_response_completion: the finite carrier, scalar repair mean, complete centered probe census, cumulative signed-load readback, and response-Gram topology are declared inputs. The result constructs no pathwise physical position, operational scale, cofinal refinement, overlap gluing, global space, clock, or fieldlayered_discrete_gauss_boundary: PR-29 supplies the c n^2 shell count, PR-30 supplies equal outward flux within each shell, and PR-31 supplies steady sourcing through the declared depth. The exponent and isotropy are therefore conditional inputs. The theorem constructs no physical radius, field, mass density, continuum limit, or Einstein-branch joincarrier_class_dispersion_band: the theorem applies to positive-weight finite mixtures of proper-carrier direction orbits with the declared cosine hop symbol, quadratic normalization, and no independent isotropic counterterm. No theorem identifies this class with a physical field or fixes its scale, frame, detector response, or exclusivitypositive_cosine_frequency_contraction: the unit constant is a certified upper bound for the auxiliary norm in the selected Euclidean carrier chart, not an optimality theorem or a physical signal-speed claim. The receipt reads no comparison data and changes no frozen bytestime_order_type_ledger: the ledger constructs no public-world endpoint, worldline, physical clock, proper-time calibration, global time function, or modular-to-time identity and emits no predictionbounded_observer_time_calibration: the event atlas, visibility, event map, clock, future-unit direction, affine unit-speed law, and shared-event equalities are supplied. No source history, refinement transport, physical instrument, SI unit, global time, modular-time identity, observable, decision rule, or prediction followsfinite_public_record_algebra_and_sharp_no_cloning: zero projectors are removed before coordinate equivalence; the mixed-state no-broadcasting implication remains an explicit adapter premise, and no physical record-selection or measurement theorem followsfinite_consensus_tower_interface: the constant adaptor proves packaging only. No nonconstant source tower, repair endpoint, causal net, geometry, clock, continuum limit, physical evolution, or prediction followsfinite_public_world_endpoint: CompletedSchedule is terminal finite completion, not infinite scheduler fairness. The A3 adaptor requires a caller-supplied seed and injective readback encoding. No source-selected physical world, cross-regulator naturality, continuum limit, clock, observable, decision rule, or prediction followscanonical_intrinsic_lorentz_module: the celestial equivalence is set-level and the frames and rest spaces are algebraic. C1 alone supplies no source-event attachment or soldering. The separate source-derived causal-order packet and bounded C2 contract supply, respectively, an informational poset and algebraic overlap covariance from declared inputs. Faithful physical placement, calibrated density, manifoldlike refinement, rods, clocks, smooth spacetime, observable, decision rule, and prediction are not constructedsource_derived_finite_one_three_causal_carrier: source height is a canonical ordinal, not a physical clock. The generic cone-inclusion theorem supplies neither its positive time scale nor a spatial readback valued in the rank-three quotient or an edge-speed bound; two-way order--cone faithfulness is the additional converse field of a faithful placement. Event-frame transports are supplied, and the standard-frame constructor is a trivial gauge choice rather than a derivation of physical observer frames. The Boolean diamond is an exact mathematical non-chain control, not empirical evidence of manifoldlikeness. No physical event/link identification, Poisson sprinkling, calibrated density or count--volume law, independent dimension estimator, topology, manifoldlike refinement, uniqueness theorem, continuum convergence, smooth metric, curvature, Einstein equation, observable, decision rule, or prediction is constructed by this finite source theorem. The separate growing-menu control supplies the frame, local move law, mesh, model layer time and event-cell measure. Its cone and interval-volume limits are analytic conditional results, not a source-selected physical manifold, Poisson sprinkling or calibrated density. The finite Lean bounds and replay do not formalize the Riemann-volume argument. The separate metric scalar limit supplies its coarsening, clipped Voronoi masses, radial-kernel force law, inertia and canonical quantization. Its analytic estimate assumes smooth references with an interaction-radius boundary buffer and h/epsilon^2 tending to zero. Five Lean lemmas check finite energy algebra, not the analytic PDE limit or physical source selection. The golden population, cube, all-neighbor read law, model tick and distinguished-event counting are declared. Its raw-count limit is not a native physical calibration, Poisson sprinkling or a finite-run dimension fit. Accepted primitive repairs, field-action agreement and laboratory clock attachment remain separate; neither the analytic volume nor pair-count proof is formalized by the finite Lean path module. The later GoldenSourceAssignment module formalizes the spatial golden partition and fixed globally Lipschitz Bochner quadrature. GoldenSourceCountLimit derives actual fixed continuity-set counts for its declared time grid. GoldenSourceCausalLimit and GoldenSourcePairLimit prove moving generated-interval and strict-pair convergence; FlatDiamondNormalization proves the one-tenth limit under window containment. GoldenSourceVolumeLimit proves the vertical weighted-volume error and limit. The separate moving-tip finite volume-error estimate remains analytic. Regional Weyl reconstruction requires supplied access to all real Weyl parameters and proves no operational quantum outcome or physical time slice. Destination-local path tomography is destructive and assumes protected memory, an isolated declared schedule and exact arithmetic; its sample-error norm does not include imperfect dynamics or decoding. A separate analytic bound g_d*(T*eta+sigma)+delta includes supplied gate, sample/retention and decoding error budgets relative to actual starting ports, without claiming sharpness for gate error or attained physical precision. Register-payload counts exclude metadata and scratch memory. Reusable transport adds supplied local classical export/reset/readout and fixed non-interleaved hops; semantic read-from projection is not physical resource order. The repeated quantum instrument supplies controlled gates, vacuum preparation, Born readout and inherited clock intervals. Its marginals are unconditional, not independent samples or branch-conditioned clocks, and its ideal scalar-action-graph pointer gadget supplies no W12 quantum routing or gate-duration/noise boundalgebraic_event_frame_soldering: the coincidence setoid, invariant readback, affine Lorentz cocycle, overlap-compatible chart-coordinate family, and base frame are supplied. Quotient descent does not construct or identify that atlas family. The source-derived packet separately supplies finite informational events and order plus an ambient 1+3 target under explicit conditions. It does not supply physical event and link attachment, two-way order-cone faithfulness, source-selected atlas coordinates, separation, open charts, calibrated count-volume density, manifoldlike refinement, topology, an operational clock, or smooth curvature. No physical spacetime, Einstein dynamics, observable, decision rule, or prediction followsfinite_causal_observer_net_interface: ordinary isotony does not supply the star-homomorphic restriction retractions or unique gluing.FiniteCoverhas no joint-coverage axiom and the B4 helper has no regional-factor attachment. The rich-fibre source payload supplies window/class labels only: its block algebra, base-point state, restrictions, and repair are declared postprocessors. Conditional coverage is attained inside that adapter, but its nonunital matrix corners are not tensor factors or aTensorSplitReceipt. The later operator-generation theorem transcribes source paths post hoc. The later 86/247 capstone grounds fully disjoint committed supports and an exact counted correlated state with the correct marginals. Its erasure theorem proves that coverage does not imply unique reconstruction. The two-observers-as-factors reading and region map remain declared. The constant-tower transport is on the separate 86/88 carrier. TripleCarrierJoin couples both pair paths, counted states, checkpoints, and adjacent-step marginals on one carrier, but supplies no regional-net or tower morphism; neither packet is a nonconstant source realization. Scientific owner #728 records the missing source-attached or otherwise justified regional construction and a nonconstant source composition; scientific owner #739 records a missing source realization or genuinely scoped no-go. No CP/CPTP channel, scheduler locality, spacetime causality, time-slice property, continuum QFT, observable, decision rule, or prediction is suppliedfinite_publicization_dynamics: the formal CP/CPTP predicate covers partition averaging, partition pinching, and the nonnegative-time relaxation channel; a positive trace-preserving transpose control is not completely positive. The operator-exponential theorem uses bounded endomorphisms of a complete real normed space. Poisson rate and forward-time interpretations require nonnegative parameters. No source-derived rate, physical clock, or prediction is suppliedfinite_public_private_dynamics: public star automorphisms are classified exactly as unique label permutations, so arbitrary pointwise-continuous public automorphism groups are trivial. Private innerness covers only one full matrix block. Arbitrary finite central sums, a coherent continuous unitary lift and single generator for every private automorphism group, source dynamics, physical time, and predictions are outside the attained packetfinite_holonomy_character_phase: the edge labels, reversal law, declared four-vertex path/face control, unitary character, cyclic sector map, and factorization are supplied. Local flatness quantifies only over the two declared faces of the four-vertex control; no puncture or noncontractibility is proved. The Aharonov--Bohm terminology is only an algebraic two-path analogy. No observer-source connection, physical gauge field, spacetime loop, charge, clock, flux, detector, laboratory fringe, or prediction is constructedfixed_regulator_operational_overlap_evidence: the access cut, restrictions, observer values, and record packet are supplied finite data. The result is not a source-production theorem and proves no cross-regulator naturality, higher-overlap cocycle, continuum observer, laboratory attachment, or predictionfinite_born_frame_rank_gap: the central atoms and spinor projectors are different objects. The projector family is a declared mathematical adapter obtained by applying a two-dimensional representation to source-realized gauge labels, not a source-produced public quantum instrument. The celestial countermodel proves that continuity and normalized antipodal binary contexts do not derive affinity; the transverse cubic refutes the displayed finite Busch--Gleason interface, and the Pauli-Y pair identifies the missing complex tomography direction. The exact phase lift constructs that direction only inside the complex operator algebra; the source has no phase producer, rotated or phase outcome receipts, common-preparation validation, or operational effect composition. Conjugation identifies one two-candidate orbit but does not prove that this orbit exhausts all hidden phase data. The repair-count bit is a post-hoc diagnostic on a locally hash-pinned B12 run; its statistic and designation rule were not preregistered, and the phase pairing is an arbitrary typed convention. The full-effect theorem applies only after full coexistent-effect additivity is supplied. No physical Born derivation, observable, or prediction is emitted. Scientific owner #730 records the missing source-earned phase instrument, operational additivity, and public readback; scientific owner #739 records the remaining affinity-principle obligationthermodynamic_four_law_package: The exact obstruction is only a bounded negative result for two direct mechanisms on the certified artifact: a mixing-mode-retaining linear intertwiner into the idempotent heat bath and a deterministic empirical pushforward. It does not exclude stochastic, nonlinear, reverse-direction, dilated, or enriched-source constructions. Scientific owner #739 records the missing replacement common reference, collar, objective, genuinely varying refinement family, source-clock derivation, and repair-export decision; empirical energy-clock calibration is PR-15. Closed #732 records only the attained conditional composition milestone. The pinned 20-state collar table has an audit of all 15 syntactic coordinate maps obtained from nonempty subsets of the four committed fields, inducing only four distinct partitions: its repair-load count aggregation is an eight-state ergodic nonreversible H-theorem probe, but it fails the pinned-table strong-lumpability diagnostic, the declared record charge is constant, and the common reference is unidentified; the fine chain's only recurrent restriction is singleton freezeout. The audit does not exclude arbitrary partitions or nonlinear, statistical, stochastic, weakly lumpable, or history-dependent maps. The strict-descent normalizer carries no entropy inequalityfinite_green_kubo_graph_transport: the reversible kernel, linear Poisson solver, graph, distance, clock increment, volumes, heat capacities, and conductances are declared finite inputs. No theorem identifies the Green--Kubo coefficient with graph conductance. The eight-state witness supplies a new faithful reference and lazy conditional resampling law; its equilibrium projection P differs from its transition T. The Poisson and tail bounds require centering within each protected fibre; a globally centred conserved record has persistent correlation. This is no native source attachment and does not overturn the historical idempotent-projector obstruction. Scientific owners #728, #729, #737, and #739 record the missing source evolution, physical equilibrium reference and conserved quantity, source-realized geometry, instrumentation, and source clock; empirical calibration is PR-15, and closed #732 is only a conditional composition milestone. The bounded algebraic C2 receipt is separate, and this row emits no prediction-ladder entryfinite_conservation_ward_precursor: the pointwise update is a declared finite premise; the load, current, update order, and charge have no physical identity. The guarded WardLimitManifest derives zero limiting residual from exact finite-residual vanishing and convergence on a shrinking scale with separating tests. Scientific owner #729 records the obligation to define that residual from finite continuity, identify it with physical distributional divergence, and supply the source, transport, chart, and common-tower evidence before continuum Ward use; scientific owner #737 records the missing instrument attachment, and #739 records deferred premise dischargefinite_fixed_word_locality_and_marginal_invariance: the repair word is fixed externally and shared by both inputs; adaptive or globally state-dependent scheduling is not covered. The cone is an upper bound, not a minimal cone or graph-radius speed law. The bipartite split is supplied, the classical theorem permits signed arrays, and no OPH region-factor, spacelike, clock, stochastic-state, CPTP, or laboratory attachment is proved. A declared rich-fibre adapter conditionally attains coverage. The later E1 packet transcribes operators post hoc and consumes this row's partial-trace helper on a declared Cartesian slot. The later 86/247 capstone grounds fully disjoint source supports and the exact counted correlated state with its marginals, while its erasure theorem proves that coverage cannot reconstruct that state. Scientific owner #728 records the missing source-attached or otherwise justified factor reading and nonconstant source composition; #739 owns the residual source realization or no-go. The missing source channel/adaptive-scheduler semantics are recorded by #728, physical clocks by #739, physical spacetime attachment by #729, instrumentation by #737, and continuum causal/time-slice structure by #730. Those scientific owners mark downstream promotions outside this claim's gate. This row emits no prediction-ladder entryconditional_adaptive_scheduler_locality_helper: sigma, R, ConsultsOnly, and every ConeRefinement map/law are supplied. The helper proves neither their source production nor fairness, liveness, positivity, normalized state/channel, CPTP, distance, clock, spacelike, continuum, or laboratory semantics. Scientific owner #728 records the missing source scheduler/channel attachment; #739 and #730 record the clock and continuum-causality attachments. This row emits no prediction-ladder entryfinite_history_variational_helpers_and_bridge_obstruction: the finite source packet and its log-transition corner action are attained, while the complete reference is not source-selected. Conditional repair of supplied trivial data under a supplied counting reference realizes only its uniform transition kernel; constant rescaling leaves that kernel unchanged, and distinct initial laws give distinct complete path references. The matching parameter exists uniquely at the supplied empirical target, but the constraint observable and level remain declared. A typed finite-to-real transfer exists only under an undercut receipt. The complete binary history law does not select the off-alphabet curvature of a regular Legendre system: the displayed family is constructed, not source-produced. The concave control concerns modes/minimizers only: constrained saddles, complex or signed stationary phase, and refinement routes are not excluded. Closed #731 records only the attained declared-bundle composition. Scientific owner #739 records source selection of the reference, real enrichment, stationary-phase mechanism, and source clock; #730 records the amplitude/interference interface, while physical fields and observable currents are not supplied here. This row emits no prediction-ladder entrymaxwell_classical_massless_kernel: the Maxwell action, positive kinetic coefficient, field content, and phase are supplied branch data; no photon Hilbert space, positive-residue pole, or universal zero-mass particle theorem is emittedyang_mills_classical_massless_kernel: this is not a free asymptotic-gluon claim and supplies neither a continuum Yang-Mills gap nor a hadron masseinstein_classical_massless_kernel: the action and background are supplied branch data; no graviton Hilbert space, quantum pole, or exclusion of additional massive modes is emittedsimple_gut_xy_channel_absent: the executable corollary applies to the declared direct-sum matrix-current fixture. Its physical current source gate is false, so the result is not a physical current or proton-stability claim. General proton stability does not follow. Conditional on the declared one-generation matter table and baryon and lepton labels, an exact dimension-six census admits QQQL, QQUE, DUQL, and DUUE; the representatives remain nonzero after the exterior-algebra relations. No coefficient, physical decay amplitude, QCD matrix element, or lifetime is suppliedlocal_face_maxwell_static_composition: finite static carrier only: no temporal electromagnetic evolution, charge-current continuity map, physical source, spacetime/continuum attachment, or readout is suppliedtriple_observer_carrier_coupling: The full step alignment, tensor slots and coherent operator lifts are declared, and pair marginals do not select the triple coupling uniquely. Observable inclusions are unital star homomorphisms; the opposite-direction partial traces are not multiplicative. The empirical state is not identified with uniform tower states or assumed transport invariant. Universal operator results belong to the Lean proof; finite Python controls are not its substitute. No source-selected quantum gate, regional-net/tower/refinement morphism, physical region, Cauchy/time-slice interpretation, physical clock or scalar64 instrument identification followscofinal_spectral_tail_four_law_composition: strict carrier growth is one sufficient refinement route; the ambient regulator, energy, inverse temperature, repair, source production, and physical continuum meaning remain declared rather than derivedseam_maxwell_continuum: Supplied R3/Lebesgue field domain, complete seam symbol, reversible curl-pair evolution, common time and same data/forcing. No source-log refinement, operational clock, physical current, finite-scale local cone, decoded observer-field/action join or laboratory identification is constructed. The result discharges no physical premise and does not arm FZ-12. Owners #728 and #754 retain the physical mapsserial_maxwell_readout: Exact classical memory and writable ports, declared potential typing, initial slices, paths, finite action, h=1/2 and Lorentz unit tau=3. No source-selected physical clock, long noisy stability, quantum copying, spatial refinement into the continuum family or laboratory identification. No physical prediction is armed or premise dischargedcone_whitney_bridge: Supplied Euclidean embedding, apex, nonlocal radial extension, Whitney Hodge pairings, unit constitutive coefficients, uniform h=1/2 interpolation and the same finite source/clock contract. The Lorentz clock action is not a volume field term, and no physical clock or SI calibration is selected. Sources are finite-element covector impulses with the declared endpoint convention, not identified physical charge/current densities. Quadratic identities require symmetric pairings; the h-squared interior defect scaling requires uniform temporal regularity for a convergence reading, and the action has an explicit endpoint defect. Spatial Gram and action/residual values are float64 controls, not interval certificates. Whitney fields have tangential/normal conformity, not global vector continuity; full sourced weak residuals retain face jumps and temporal impulses and do not vanish here. Checking all finite-element coordinates does not establish arbitrary-test continuum stationarity. No refinement family, source-selected physical geometry, continuum convergence, measured postdiction, new prediction or premise discharge is suppliedwhitney_maxwell_dynamics: Supplied Euclidean cone, constitutive interpretation, h=1/2, changed initial electric field, prescribed impulse source covectors, dense software evolution and exact writable classical ports. Exact mass positivity and the stability bound are derived for that geometry, not physical source selection. The local signed-coordinate certificate policy and global real face-order policy are separately proved; their bundle establishes no common local/global transport. Lean-free checks authenticate the committed witness payload and source closure plus numerical agreement; full kernel and consumer replay requires Lean. Float64 trajectory with 1e-9 comparison tolerances is not an interval trajectory certificate. Only three slices per gauge are instrumented. Finite-element stationarity is not arbitrary-test continuum stationarity; no physical clock, spatial refinement, laboratory evidence or new prediction.whitney_radiative_quantum: Canonical quantization and hbar are imported. Lean constructs the complete positive normal frame from the certified mass forms of the supplied geometry. The local exact signed-coordinate certificate transport and global real face-order transport have separate naturality proofs; no common local/global policy is established. Hilbert completion, operator closures and temporal convergence are paper proofs. This is the zero-charge source-free radiative sector, not quantization of the prescribed-charge episode or interacting matter action. sqrt(lambda) and finite-step theta/h are distinct; no uniform operator-norm quantum error, spatial continuum limit, selected Born statistics or physical clock is supplied.whitney_charged_matter: Supplied scalar species, charge, mass, nonnegative quartic coefficient, Euclidean geometry, time and exact pulled-back scalar-QED Lagrangian. Real unwrapped edge integrals are needed. Differentiate the gauge-dependent scalar basis in all field variations; a naive projected scalar current omits terms. All thirteen scalar variations require total neutrality in the declared boundary convention. This algebra/global-existence result alone supplies no executed charged-matter episode, spatial error estimate or interacting quantum completion; those distinct constructions have separate rows. No source-selected matter content or Standard Model identification is supplied.whitney_spatial_consistency: Supplied geometry, smooth bounded fields, conforming shape-regular refinements, action time parameter and scalar-electrodynamics density. The uniform estimate is an analytic paper theorem, not a Lean convergence theorem or a bound certified by finite samples. Exact edge integration and the Whitney interior-path definition are required. No nonlinear trajectory convergence, arbitrary-H1 nodal estimate, observer source selection, calibrated physical clock or empirical comparison is established.whitney_interacting_quantum: Supplied fixed cone, scalar species/action, nonzero charge, nonnegative mass-squared/quartic coupling, hbar, quantization measure, Laplace--Beltrami ordering and Gaussian width. The Schur complement uses the full coupled kinetic metric, which includes every block beside the Maxwell one. Essential self-adjointness removes extension ambiguity for this declared operator, not the quantization choices themselves. The metric constants depend on the fixed mesh and couplings and are not uniform continuum-refinement estimates. The analytic proof is not formalized in Lean. The chosen Gaussian is not a derived vacuum or physical preparation. No unique quantization, equivalence to quantization before reduction, continuum interacting QFT, computed quantum-state history, physical Born statistics or laboratory identification is supplied. The shared-observable theorem uses real bounded scalar smearings and square-integrable magnetic smearings. Its continuum detector corollary retains the zero-current real sector, m^2>0, smooth Neumann reference, conforming refinement and Ritz data. These are analytic results, not numeric proofs of multiplication self-adjointness or quantum refinement. No ground-state assumption, quantum-classical state identification or physical detector calibration follows. General bounded Borel detectors have no asserted classical continuum convergence rate.whitney_charged_execution: Supplied dimensionless cone, scalar action, e=1/4, m^2=1/2, g=1/4, temporal gauge, initial data and action parameter on [0,2]. Exact-real symmetry and polynomial quadrature arguments are separate from floating-point samples. Sample residuals, independent integration and fixed-step comparisons do not enclose trajectory error rigorously. The trajectory occupies the fixed five-coordinate sector, with zero magnetic field but nonzero electric interaction and matter motion. No authenticated observer execution, actual quantum state, spatial continuum trajectory limit, physical clock or measured postdiction is supplied.whitney_real_continuum: Supplied cone and continuum time, scalar species/action, m^2>0, g>=0, real neutral sector, natural Neumann boundary conditions, and an existing C^2_t H^2_x continuum reference. The theorem requires Ritz-compatible initialization. The stored pulse trajectories instead use nodal initialization and verify numerical implementation, not the continuum error bound. No full charged-complex trajectory convergence, numerical interval enclosure, source-selected geometry/matter/clock or empirical comparison is established.whitney_charged_instrument: Supplied symmetry-coordinate patch placement, classical writable registers and records, numerical solver, cone, scalar action, initial data and action step. Hash-pinned replay proves internal software provenance without external attestation. The five patches are computational coordinates, not physical observer locations. Repair counts are operational events; their assignment to model time is supplied. The original numerical residuals are not rigorous trajectory enclosures. The separate checkpoint certificate transfers the historical sample bound by an exact rational triangle inequality; it does not enclose intermediate probe registers, continuous observer evolution, nonlinear field or configuration-clock readouts. No quantum history, continuum trajectory limit or laboratory clock calibration is attached.whitney_ephemeris_clock: Supplied full action, energy, temporal gauge, configuration-coordinate convention and ordered classical path. The analytic statement requires positive kinetic energy and E-V>0 and excludes turning points. The numerical polyline and quadrature comparisons do not certify segment-wide admissibility or integration/trajectory errors. Source authentication may inspect record metadata; the duration calculation consumes configurations only. This model-internal duration has no selected physical units, laboratory calibration, Lorentzian spacetime identification or quantum-clock operator.whitney_quantum_history: Supplied interacting action, Hilbert measure, operator ordering, hbar, Gaussian width and Hamiltonian time. This is a potential-phase trial with a conservative dimensionless horizon 2^-55 and norm-error target 1/10, not a computed exact Hamiltonian history or a practical ordinary-physics simulation. Global analytic envelopes and exact Gaussian moments avoid numerical quadrature or omitted Gaussian tails in the bound. No evolving configuration density, observer preparation, physical clock, continuum QFT or empirical comparison is established.spin_exchange_selection_boundary: The same full internal state, preparation, ideal detector and error budgets are supplied. There are no native or laboratory outcomes; operator Gauss of the one-particle parent does not transfer to this new preparation.conditional_pauli_scalar_q_selection: The quantization class, unit phase law and finite full representation or stable quantum ladder are declared. The source response Hilbert space is not identified with the full matter representation. The theorem is spin independent; truncated bosons and other classes remain outside its premise.conditional_pauli_operation_selection: Under the exact phase law contraction is equivalent to exclusion. The field/Kraus identification and exact unit normalization are supplied, not source-derived. General normalized instruments can have an idle outcome and do not force these hypotheses. The finite countercontrol is not a full A1-A3 model or impossibility theorem. Physical Spin, native operation and matter attachment remain unproved.
The exact conditional four-dimensional propagating-mode vector is (2, 16, 2): two Maxwell modes from one U(1) generator, sixteen perturbative color modes from eight SU(3) adjoint generators, and two Einstein transverse-traceless modes from one metric tensor field. The entries are neither particle counts nor one uniform gauge-algebra dimension vector.
| Carrier | Quantum verdict | Blocking frontier |
|---|---|---|
photon |
NOT_EVALUABLE_NO_SOURCE_SELECTED_MAXWELL_QUANTUM_SECTOR |
source_selected_unbroken_u1_quantum_maxwell_sector, finite_source_to_lorentzian_quantum_eft_construction |
gluon |
NOT_EVALUABLE_NO_QCD |
finite_source_to_lorentzian_quantum_eft_construction, source_derived_qcd_physical_spectral_sector |
graviton |
NOT_EVALUABLE_NO_PHYSICAL_SOURCE_CAUSAL_CONTINUUM_OR_QUANTUM_CARRIER |
source_selected_faithful_3p1_causal_manifold_and_smooth_einstein_limit, finite_source_to_lorentzian_linearized_quantum_carrier |
The target-named status packet consumes no laboratory comparison value, permits no particle promotion, and is ineligible as a blind prediction. Its receipt is code/particles/runs/status/quantum_carrier_status.json.
alpha_em^-1Thomson endpoint:136.3827548in[136.3670481, 136.3984652]against CODATA137.0359992(compare-only). Payload releaseknt19_pinned_v1.- Recorded retrospective same-scheme accounting interval
[0.6199, 0.6506]inverse-alpha units; the standard reference deficit sits inside that interval. - Independent-class verdict:
MULTI_CLASS_NOT_EVALUABLE__ONE_RECORDED_ACCOUNTING_REPLAY_COMPATIBLE; evaluated independent classes:0. - Reading: one retrospective KNT19 accounting row is arithmetically compatible with the recorded same-scheme interval. The multi-class HVP test is not evaluable because no independent frozen class is present. Containment does not identify the physical source of the gap, select one closure map, construct the same-quantity bridge, or close source-only transport
- Scientific owner: #736
The closure map of the pixel lane has a certified fixed point in each declared mode, and the lane reads as a chain: the fixed point of the root map, the fixed point of the same map with the unified gauge width, and the term between that second fixed point and the reference value. Each row is compare-only: the CODATA reference sits outside every solve path, and the certificate permits no promotion.
| Closure map | Fixed point alpha_em^-1 |
Enclosure width | P |
Distance to CODATA | Relative |
|---|---|---|---|---|---|
| root closure map, unified gauge width absent | 136.994835177 |
7.2e-24 |
1.63097209586 |
-0.041164 |
-3.00e-04 |
| closure map with the finite-screen unified gauge width on the inverse coupling | 137.035660137 |
7.1e-24 |
1.6309682414 |
-0.000339 |
-2.47e-06 |
alpha_inv_closure_root: alpha -> 1/(alpha_em^-1(m_Z^2;P) + Delta_Th(P)) with P = phi + alphasqrt(pi); Delta_Th is the internal Stage-5 structured Thomson continuation with the exact one-loop fermion kernel and quark screening factor 1 - N_calpha_3(m_Z;P)/pi. Existence and uniqueness of the fixed point are certified by interval arithmetic with Lipschitz bound0.0724at cutoffs120and90, with the tails bounded.alpha_inv_closure_gauge_width: alpha -> 1/(alpha_em^-1(m_Z^2;P) + Delta_Th(P) + alpha_U(P)) with P = phi + alpha*sqrt(pi); the closure-ledger CL-2 mixed map that adds the finite-screen unified gauge width alpha_U(P) to the inverse-alpha readout. Existence and uniqueness of the fixed point are certified by interval arithmetic with Lipschitz bound0.07235at cutoffs120and90, with the tails bounded.- The distance from the gauge-width fixed point to the CODATA reference,
0.000339inverse-alpha units, is the open term of this lane. It carries the hadronic content that the Thomson-endpoint row above accounts for retrospectively, and closing it from the source side is work in progress under the scientific owner #736. - Neither closure row is a frozen prediction, and neither is eligible as a blind prediction: both are retrospective comparisons of a certified fixed point against a reference value.
- Closure target (T1_empirical_closure): the anchor-gap value
0.6379closes the lane exactly on the measured triple (inversion machine-checked); the distance+0.0070to the on-shell reference deficit0.6309is the unfixed scheme term of the bridge. The certified width floor is the scheme-band ambiguity; no budget is shrunk without the source bridge. - MCPR conditional triple (T2): electron
-84.1 ppm, muon-84 ppm, tau-84 ppmagainst the PDG witness triple; the eight-register architecture is a declared model input. - Kappa interval, rectangle (T1_empirical_closure): outward-rounded target-anchored diagnostic intervals with logarithmic half-width
6.554%and one-sided multiplicative widths-6.34%/+6.77%; the witness triple lies inside every interval. - Kappa interval, coherent closure (T1_empirical_closure): outward-rounded target-anchored diagnostic intervals with logarithmic half-width
1.732%and one-sided multiplicative widths-1.72%/+1.75%; the witness triple lies inside every interval.- Width reduction over the rectangle:
3.78x; premise: payload-coherent anchor-gap premise, declared.
- Width reduction over the rectangle:
- Koide conditional tau (T2_conditional): under the balanced-circulant and mass-ordering premises the measured electron and muon masses fix the tau mass inside
[1776.968991, 1776.969063]MeV,0.4336sigma from the measured1776.93 +- 0.09MeV; the premise ancestry is declared and improving tau-mass averages test the premise directly.
| Quantity | Conditional central | Envelope | Measured | Delta/sigma | Status |
|---|---|---|---|---|---|
mH_gev |
125.20748 |
[125.18329, 125.23167] |
125.13 +- 0.11 (PDG 2026) |
0.704 |
compare-only |
mt_pole_gev |
172.31492 |
[172.27749, 172.35236] |
172.1 +- 0.6 (PDG 2026 cross-section pole-mass context row) |
0.358 |
compare-only |
MW_chart_gev |
80.373315 |
[80.369217, 80.377413] |
chart coordinate | n/a | NOT_EVALUABLE |
MZ_chart_gev |
91.193124 |
[91.187978, 91.198269] |
chart coordinate | n/a | NOT_EVALUABLE |
W/Z rows are running/tree chart coordinates. The strict one-loop consumer has a separate external fixture: interval receipts exclude scalar zeros in the declared principal-sheet boxes and isolate, for each of W and Z, one simple scalar zero with derivative and scalar-residue balls in its declared lower-half pole box on a channel-specific algebraic chart. They identify neither chart with the physical resonance sheet and prove no unique continuation, sign bridge, full-matrix Laurent residue, physical-current amplitude, or independent numerical replay. The fixture is not composed with the OPH chart, so no physical W/Z pole or mass comparison is defined. The Higgs and top rows are conditional on the declared selection axioms.
- Absolute masses (source_only_nonidentifiability_obstruction_transport): No absolute quark mass is emitted. The two-modulus spread fiber (R>0)^2, obtained by granting a candidate-only ordered shape law, survives the 2026-07 certified structure set (matter receipt #314, port receipt #566, twelve frozen selector candidates, with input hashes pinned at emission), so the six source-only absolute masses are non-identifiable from that set, by an explicit rescaling symmetry of the registered data. Live cuts: a Yukawa-typed source equation through the physical bindings or the family attachment, a new selector under the frozen discipline, or the conditional Higgs/top criticality coordinate (scientific owner #736).
- Down-type register-Clebsch route, rejected (T2_conditional_rejected_candidate):
ms/md = 22.97against FLAG 2024 (Nf=2+1+1: 19.94, Nf=2+1: 20.36); all six generation assignments are rejected by the retrospective conservative gate. The diagnosticsqrt(md/ms) = 0.2086is not a derived Cabibbo angle. Premise: a cross-sector register relation, independent Yukawa coefficient identification, and a physical generation order; the pairing receipt supplies channel compatibility only. The target-free F1/F2 scan fixes only the unordered multiset. All six assignments fail the retrospective conservative FLAG gate. The displayed GST value is sqrt(md/ms) under an assumed texture, not a derived CKM angle; a simultaneous diagonal mass ansatz would instead give the identity CKM matrix.
- Correction engine payload:
Delta alpha_had^(5)(M_Z^2) = 0.027609 +- 0.000112fromknt19_pinned_piecewise_v1(pin factor1.03176). The published-compilation payload is the correction engine of the fine-structure lane; source-only hadron rows stay suppressed. The resource-deferred QCD backend supplies no source-only result; scientific owner #736 records the bounded particle-output obligation, and source-only QCD remains outside the available resources. - QCD solver:
SOLVER_COMPILED_AND_SMOKE_BLOCKED_INVOCATION_GATED_ON_SOURCE_PARAMETERS; invocation is gated on the source-side parameter emissions recorded in the standby receipt. - Transmutation scale (T2_conditional):
Lambda_QCD^(3) = 0.334815GeV in[0.319493, 0.34975]against the published central0.338GeV (compare-only),-0.94%relative. Threshold locations are declared external quark scheme masses, and the interval is the swept threshold bracket. Lambda is the perturbative transmutation scale of the source coupling. Hadron masses additionally require the nonperturbative ratio m_h/Lambda, which this lane does not supply. - Nucleon mass (T2_conditional):
0.929112GeV in[0.82319, 1.04253]against the measured proton mass0.93827GeV (compare-only),-0.98%relative, with the measured value inside the interval. The declared external lattice-theory ratio is2.775with uncertainty0.105. This is a conditional hadron mass: source transmutation times a declared external lattice-theory ratio. A source-only hadron mass requires the production hadron backend.
- dimensionless PMNS and mass-splitting-ratio comparisons are recorded on the results surface; the absolute attachment stays compare-only (
code/particles/RESULTS_STATUS.md).