The Current Takes the Stand

Claims and proofs

Every claim is registered in the claim map. Open one to see its statement, where it appears in the paper, and the Lean modules and replay programs that prove it. Statements registered in Chinese are shown in English translation.

In reading order. Black: proved in Lean, kernel check passed; grey: supported by replay programs, no Lean declarations.

1. §1One current, three calculations
2. L17A norm-continuous history R of bounded self-adjoint operators (boundedness on each compact time interval suffices) generates, for every real ε, every initial and final time, and every L² initial state, actual development, uniqueness, norm conservation, two-time unitary propagation, and the original weak equation.§1

   A norm-continuous history R of bounded self-adjoint operators (boundedness on each compact time interval suffices) generates, for every real ε, every initial and final time, and every L² initial state, actual development, uniqueness, norm conservation, two-time unitary propagation, and the original weak equation. At each fixed real time, the actual propagator has the operator-norm derivative D(t) at ε=0; the derivative of the original field is the original-time Duhamel integral, and the derivative of the original current is the same Kubo kernel and Stage10 response. A control with zero past keeps the free past, and the preparation phase is preserved.

   Location: §1; §8; D.2; D.4; Figure 3✓ Kernel check passed

   Lean modules · 4

   • Physics.LowEnergyMatterSpace.GlobalGlue1 declarations

     perturbed_global_exists
   • Physics.LowEnergyMatterSpace.GlobalFlow1 declarations

     globalPerturbedDevelopment
   • Physics.LowEnergyMatterSpace.PerturbedVariation1 declarations

     perturbed_quadratic_remainder
   • Physics.LowEnergyMatterSpace.PerturbedOperator1 declarations

     couplingOperator_derivative
3. §2The original action, nine fields, and the time dictionary
4. L1Substituting the original single-copy Weyl inventory plus a complex Λ⁴ scalar into the existing one-loop algebraic formula gives b₀ as (56/3,4,1/3,−28).§2

   Substituting the original single-copy Weyl inventory plus a complex Λ⁴ scalar into the existing one-loop algebraic formula gives b₀ as (56/3,4,1/3,−28). The three original constitutive parameters are all 1/2; the mother U(1) trace pairing is twice the native pairing. In the specified coordinate, I₃=1+4t, I₂=1+t/3, and I₁=1/2−7t are simultaneously positive on −1/4<t<1/14, and the three lines have no common intersection.

   Location: §2; A.1✓ Kernel check passed

   Lean modules · 3

   • Physics.LowEnergy.ScalarInventory1 declarations

     b0_table
   • Physics.LowEnergy.Normalization1 declarations

     native_boundary
   • Physics.LowEnergy.Running1 declarations

     normal_forms
5. L2The complete 7×21 Yukawa matrix of the original four-term vacuum satisfies YY†=diag(2,2,2,4,2,0,0), with rank 5 and a 16-dimensional input kernel.§2

   The complete 7×21 Yukawa matrix of the original four-term vacuum satisfies YY†=diag(2,2,2,4,2,0,0), with rank 5 and a 16-dimensional input kernel. The original P286 scalar–gauge quadratic block has rank 9 and spectrum 0[3],1[6] together with the three roots of 6x³−26x²+27x−8. The stabilizer of the bare scalar in the compact mother group is (SU(2)×USp(4)×U(1))/Z₂, and its intersection with P286 is the specified embedded SU(2).

   Location: §2; A.2–A.3✓ Kernel check passed

   Lean modules · 1

   • Physics.LowEnergy.JointMassCoordinates2 declarations

     coefficient_actualoutputGram_actual

   Replay programs and evidence · 1

   • exact_readout.py
6. L4The original exterior-power basis and the four Dirac components generate the 252 complex coordinates and the complete operator algebra; compression retains the return term C(AB)=C(A)C(B)+C(AQB).§2

   The original exterior-power basis and the four Dirac components generate the 252 complex coordinates and the complete operator algebra; compression retains the return term C(AB)=C(A)C(B)+C(AQB). On the same generated nine-field configuration, the independent-dual response is χ(Aψ)=4s a⁻³⟨ψ̂θ,SAψ̂θ⟩, and the actual density satisfies a³ρ=4s.

   Location: §2; §3.4; D.3✓ Kernel check passed

   Lean modules · 3

   • Physics.LowEnergyQuantum.Compression1 declarations

     compression_product
   • Physics.LowEnergyQuantum.Readout1 declarations

     moving_response
   • Physics.LowEnergyQuantum.Density1 declarations

     spatial_volume_response
7. L7The Q=γ⁵+2P₆ phase transformation on the complete 252-dimensional carrier makes the original operator stationary, and original time is restored by the same phase.§2.5

   The Q=γ⁵+2P₆ phase transformation on the complete 252-dimensional carrier makes the original operator stationary, and original time is restored by the same phase. The existing canonical preparation tangent satisfies K₈₈=CᵀH₁₁₂C, H₁₁₂C=RK₈₈, and CᵀR=I; the nine symmetry directions generate a 79-dimensional quotient, and the 103-dimensional system splits faithfully into 79+24. The maximal development fiber of the peripheral canonical sector has dimension 522 generically, 524 at the origin, and 530 on the sphere |k|²=5929/1800, and all 1078 original rows are written back.

   In addition, the Yukawa mixing kernel of the original 70 real scalars and the orthogonality condition to the real gauge orbit generate a 43-dimensional background-invariant space, adapted into 23 real singlets and 5 four-real-dimensional blocks. The program supplies the source matrix and the adapted basis; the formal Lean proof supplies the determinants and inverses of the four-dimensional blocks and the substitution of the original parameters.

   Location: §2.5; §4.4–4.5; B.2✓ Kernel check passed

   Lean modules · 2

   • Physics.LowEnergyFullPhase.Operator2 declarations

     gamma_preservedyukawa_preserved
   • Physics.LowEnergyFullPhase.Derivative1 declarations

     kinetic_phase_term

   Replay programs and evidence · 4

   • compute.py
   • compute.py
   • compute.py
   • compute.py
8. §3Joint nine-field development and its actual tangent
9. L3Near every admissible seven-dimensional spatially homogeneous initial value there exist a common positive initial-data radius, a two-sided time interval, and a uniform Lipschitz solution family, and the entire closed initial-data ball generates complete joint zero residuals of all nine fields.§3.1–3.2

   Near every admissible seven-dimensional spatially homogeneous initial value there exist a common positive initial-data radius, a two-sided time interval, and a uniform Lipschitz solution family, and the entire closed initial-data ball generates complete joint zero residuals of all nine fields. At the original background seed, the Fréchet derivative with respect to initial data is exp(tJ) and satisfies the same Jacobi equation; the base point of the derivative remains the original seed.

   Location: §3.1–3.2; B.1✓ Kernel check passed

   Lean modules · 2

   • Physics.LowEnergyEvolution.Uniform1 declarations

     uniformDevelopment_exists
   • Physics.LowEnergyEvolution.VariationDerivative2 declarations

     initial_derivativeinitial_fderiv
10. L5The original radial equation is ∂t²f/N²−Δf−2f=0.§3.3

    The original radial equation is ∂t²f/N²−Δf−2f=0. For every real three-momentum, the fundamental solutions are given by sinh, the critical linear function, and sin, respectively, with zero initial value and initial velocity cos(k·x). Substituted back into the original nine fields, eight classes of residuals vanish exactly and the complete coframe residual is ε² times the original second-order load, so the first variation of the nine fields vanishes.

    Location: §3.3✓ Kernel check passed

    Lean modules · 1

    • Physics.LowEnergySpacetime.Propagation2 declarations

      fundamentalTime_equationfundamentalWave_operator
11. §4Full coupled propagation and reconstruction of the original fields
12. L6The quadratic action on the first-order jet of the original 289 real fields is eliminated successively to 217, 145, and 121 variables; Ward row transformations retain 112 equivalent equations.§4.1–4.3

    The quadratic action on the first-order jet of the original 289 real fields is eliminated successively to 217, 145, and 121 variables; Ward row transformations retain 112 equivalent equations. A constant invertible minor of the nine source-symmetry directions generates a 103-dimensional section; the rank at the origin is 98, and the additional five-dimensional kernel is retained. The ten axial blocks produce 22 distinct rational factors with total time degree 126; simultaneous spatial/spin/color rotation transports the complete original fields and equations to every real three-momentum, and the radial catalog has 14 factor-product blocks.

    Location: §4.1–4.3; B.2

    Replay programs and evidence · 5

    • compute.py
    • propagation.py
    • generators.py
    • finite.py
    • catalog.py
13. §5The low-momentum action of two phases
14. L8Eliminating the 77 directions invertible at the origin from the original canonical 79-dimensional operator gives the effective action of the original vector phase ϕ and axial phase θ, quadratic in amplitude and through fourth derivative order.§5

    Eliminating the 77 directions invertible at the origin from the original canonical 79-dimensional operator gives the effective action of the original vector phase ϕ and axial phase θ, quadratic in amplitude and through fourth derivative order. The low-momentum branches are

    $$\lambda_\varphi^2=-\frac{594}{1675}|k|^2-\frac{10152864}{939884375}|k|^4+O(|k|^6),\qquad \lambda_\theta^2=\frac13|k|^2-\frac{3053}{29160}|k|^4+O(|k|^6).$$

    Location: §5; B.3; Figure 2

    Replay programs and evidence · 2

    • compute.py
    • receipt.json
15. §6How the original external legs exchange interaction
16. L9The complete 252-dimensional matter carrier produces 158 vertices: 48 gauge, 24 Lorentz, 16 coframe, and 70 scalar.§6.1–6.3

    The complete 252-dimensional matter carrier produces 158 vertices: 48 gauge, 24 Lorentz, 16 coframe, and 70 scalar. The 97 active sources enter the 79+24 dynamical blocks, the auxiliary contact terms, and the nine rows of source compatibility conditions; the 24 complementary-block vertices of prepared real sources vanish. The connection inverse gives the axial four-fermion term 3N/16 η_ab AᵃAᵇ. The 61 peripheral scalar sources are consumed by the actual projected inverse, and the nonzero Yukawa return and the independent-dual equations are retained.

    Location: §6.1–6.3; C.2✓ Kernel check passed

    Lean modules · 2

    • Physics.LowEnergyExchange.Current1 declarations

      original_current
    • Physics.LowEnergyExchange.Static1 declarations

      original_current_exchange

    Replay programs and evidence · 3

    • compute.py
    • exchange.py
    • compute.py
17. L10The original free projections generate the 216-complex-dimensional Hermitian spectrum at all momenta, the original/co-rotating frequencies, and external legs in the 252 coordinates.§6.4–6.6

    The original free projections generate the 216-complex-dimensional Hermitian spectrum at all momenta, the original/co-rotating frequencies, and external legs in the 252 coordinates. The two actual Dirac equations pay for the 18 source conditions; both orderings of the genuinely conserving four external legs consume the complete 79-dimensional dynamical block and write back the 289 rows. The kinetic term and residue of the original action fix the normalization; the right-handed scale 2^(−1/4) has been verified, and the corresponding four-leg tree coefficient is exactly halved.

    Location: §6.4–6.6; C.1; C.3✓ Kernel check passed

    Lean modules · 2

    • Physics.LowEnergyKinetic.Density1 declarations

      original_action_time_affine
    • Physics.LowEnergyKinetic.Scale1 declarations

      normalized_right_unit

    Replay programs and evidence · 6

    • compute.py
    • spectral.py
    • external.py
    • scalar_readback.py
    • compute.py
    • compute.py
18. L11The original Hodge elimination gives L=N/(2σ)κ(E,E)−1/(2σN)κ(B,B).§6.7

    The original Hodge elimination gives L=N/(2σ)κ(E,E)−1/(2σN)κ(B,B). After the proper clock, the connection one-form, and the density are transformed together, the electric/magnetic inverse coefficients in the native pairing are 108/125 and 125/27; the characteristic-speed ratio of the transverse gauge wave to the original matter/scalar fields is 125/54 (original-coordinate speeds 1/N and N, respectively). The 12 static charge sources write back the 289 rows, the 144 charge responses are regular at zero momentum, and the zero-momentum Coulomb residue vanishes in every direction.

    Location: §6.7; C.3; §14.1

    Replay programs and evidence · 3

    • compute.py
    • compute.py
    • compute.py
19. §7From the occupied current to an actual spatial preparation
20. L12The original H₁₂=spin₄⊗span{e₀₅,e₁₅,e₂₅} is closed under all 48 gauge forces.§7.1

    The original H₁₂=spin₄⊗span{e₀₅,e₁₅,e₂₅} is closed under all 48 gauge forces. The matter equations on both legs generate the 48×48 response, which equals the matter Schur elimination of the original 289-field action; all 2304 entries are checked term by term at three sample points where the inverse exists. At zero spatial momentum, the same response is recovered from the positive-time equation, the delta jump, and the positively damped half-axis integral, retaining the original zero mode.

    Location: §7.1

    Replay programs and evidence · 2

    • compute.py
    • compute.py
21. L13The original 12-dimensional occupied coefficients generate strongly continuous unitary development on L²(ℝ³,ℂ¹²), a Bochner forced solution with zero past, and uniqueness of mild solutions with the same initial value.§7.2–7.3

    The original 12-dimensional occupied coefficients generate strongly continuous unitary development on L²(ℝ³,ℂ¹²), a Bochner forced solution with zero past, and uniqueness of mild solutions with the same initial value. The actual self-adjoint generator satisfies f∈Dom(H) ↔ h(2πξ)f̂∈L², and Schwartz tests read back the original partial-derivative operator. The genuine holonomic original field gives H_original(0)=h₀+ωQ in the same coefficients; the original independent-dual weak form is preserved.

    Location: §7.2–7.3; D.1✓ Kernel check passed

    Lean modules · 3

    • Physics.LowEnergyMatterSpace.Source1 declarations

      sourceHamiltonian_hermitian
    • Physics.LowEnergyMatterSpace.Spatial1 declarations

      spatialUnitary_add
    • Physics.LowEnergyMatterSpace.GeneratorDomain2 declarations

      source_domain_iffsource_hamiltonian_value
22. L14A continuous L² gauge-control history produces, through the actual Duhamel integral, a bounded preparation map K; for every real time t, the norm bound is $\|K_t\|\leq|\int_0^t\|F(\tau)\|\,d\tau|$.§7.3

    A continuous L² gauge-control history produces, through the actual Duhamel integral, a bounded preparation map K; for every real time t, the norm bound is $\|K_t\|\leq|\int_0^t\|F(\tau)\|\,d\tau|$. The original occupied vector gives Kρ₀K†. A genuine nonzero control generates a nonzero preparation at some positive time, which after normalization is a unit positive functional. A complete spatial observable A is first pulled back to K†AK and then forms the 252-dimensional mother action; pairedMother 1 applies the original spin exchange S after the complete operator, and the factor 4 spinScale of the independent-dual readback is preserved; see (7.13a) and (D.2) in the main text.

    Location: §7.3; D.3✓ Kernel check passed

    Lean modules · 2

    • Physics.LowEnergyMatterSpace.PreparationHistory1 declarations

      preparationMap_norm
    • Physics.LowEnergyMatterSpace.PreparationGauge1 declarations

      gauge_history_prepares_nonempty
23. L15The common span of any finite L² test family and the preparation vector provides a genuine finite Fock carrier; the CAR recursion produces all finite word moments, adjoint positivity, and consistency under enlargement of the test family.§7.4

    The common span of any finite L² test family and the preparation vector provides a genuine finite Fock carrier; the CAR recursion produces all finite word moments, adjoint positivity, and consistency under enlargement of the test family. The tests may be nonorthogonal, linearly dependent, or repeated. The complete word is first composed in the Fock space and then enters the mother-action reading through J†WJ and the same preparation map.

    Location: §7.4; D.3✓ Kernel check passed

    Lean modules · 2

    • Physics.LowEnergyMatterSpace.SpatialCARWords1 declarations

      wordOperator
    • Physics.LowEnergyMatterSpace.SpatialCARState1 declarations

      spatialMoment_positive
24. L16The original P286 action generates the local bounded self-adjoint force T and current B, B=−spinScale QT; the genuine L∞×L² multiplication makes the current density integrable.§7.5

    The original P286 action generates the local bounded self-adjoint force T and current B, B=−spinScale QT; the genuine L∞×L² multiplication makes the current density integrable. Duhamel gives the two-sided response i∫⟨u,[R_H(s),B_H(t)]u⟩ds, consumed jointly by the complete CAR four-point word and the original Stage10. Original time is restored by U_original and the total preparation phase P(t+preparedAt); multitime CAR words retain the phase leg by leg.

    Location: §7.5; §8.3; D.4✓ Kernel check passed

    Lean modules · 2

    • Physics.LowEnergyMatterSpace.CurrentOperator1 declarations

      gaugeCurrentMatrix_weight
    • Physics.LowEnergyMatterSpace.SpatialResponseKubo1 declarations

      currentVariation_kubo
25. §9How the same source prepares electromagnetic readouts
26. L18Joint full-exterior/scalar/matter/independent-dual EM action generates relative real CAR increments +/-1/2 and retains the input/scalar charge remainder.§9.1–9.4

    Joint full-exterior/scalar/matter/independent-dual EM action generates relative real CAR increments +/-1/2 and retains the input/scalar charge remainder. The actual composite current has J_i=0 for i>=73 and F0^T J=(e0+e1)w_J, with complete native/coframe/density/matter/complement/retained configuration integral and both original inverse prices. Each unit real spatial direction gives the whole static Schur/contact/complement return, -kappa^2 residue and original O(kappa) finite-factor bound.

    Location: §9.1–9.4; §9.5; Appendix F.2✓ Kernel check passed

    Lean modules · 6

    • LowEnergyPhenomenology.AlphaSource.SourceJointPhaseAction5 declarations

      sourceJoint_exteriorsourceJoint_readsourceJoint_dualsourceJoint_creation_chargesourceJoint_annihilation_charge
    • LowEnergyPhenomenology.AlphaSource.SourceJointPreparedCoupling5 declarations

      sourceJointInputCore_generatedsourceJointCompleted_chargesourceJointChargedCurrent_generatedsourceJointPhotonEmitter_generatedsourceJointPhotonCoupling_generated
    • LowEnergyPhenomenology.AlphaSource.SourceStaticCompositeProjection2 declarations

      sourceStaticComposite_inactivesourceStaticComposite_origin
    • LowEnergyPhenomenology.AlphaSource.SourceStaticCompositeCurrent5 declarations

      sourceStaticCompositeGauge_slotssourceStaticCompositeConfiguration_generatedsourceStaticCompositeWeight_generatedsourceStaticCompositeWeight_pricesourceStaticCompositeLeading_return
    • LowEnergyPhenomenology.AlphaSource.SourceStaticSpatialTensor3 declarations

      sourceStaticSpatialTensor_generatedsourceStaticSpatialKernel_neumann_pricesourceStaticSpatialKernel_inverse_delta
    • LowEnergyPhenomenology.AlphaSource.SourceStaticSpatialCoupling5 declarations

      sourceSpatialStaticNativeFieldWholesourceSpatialStaticNativeFieldSchursourceSpatialStaticNativeFieldResiduesourceStaticSpatialContraction_pricesourceStaticSpatialInteraction_generated
27. L22The same source-generated SourcePreparation supplies sourceProfile, its configuration-background unit state, nativeY=-1 and completed source legs.§9.2

    The same source-generated SourcePreparation supplies sourceProfile, its configuration-background unit state, nativeY=-1 and completed source legs. The full photon amplitude A and A/(h_source*c_source), with complete polarization/double-resolvent bound and full-Y domain/cutoff, form the generated typed ordinary input.

    Location: §9.2; §9.5; Appendix F.1✓ Kernel check passed

    Lean modules · 2

    • LowEnergyPhenomenology.AlphaSource.SourcePreparedPhotonAmplitude5 declarations

      sourcePreparedPhotonProfile_generatedsourcePreparedPhoton_unitsourcePreparedPhoton_chargesourcePreparedPhotonAmplitude_normalizedsourcePreparedPhotonAmplitude_price
    • LowEnergyPhenomenology.AlphaSource.SourcePreparedThomsonInput3 declarations

      SourcePreparedThomsonInputsourcePreparedThomsonInputsourcePreparedThomsonOrdinaryFull_normalized
28. L20The literal EM direction generates exterior weights and the dressed joint charge unit 1/2.§9.3

    The literal EM direction generates exterior weights and the dressed joint charge unit 1/2. Creation and annihilation characters are +i/2 and -i/2. The complete prepared covector is (conj(c_left)+c_right)J on the same completed profile. GT character/completed/current readers are the real multiple -10/11, without equality of full generators.

    Location: §9.3✓ Kernel check passed

    Lean modules · 2

    • AlphaSource.EmIdentification.PhysicalEMDressedCharacter3 declarations

      emDressedChargeUnit_valueem_dressed_readem_dressed_dual
    • AlphaSource.EmIdentification.PhysicalEMDressedPreparedRead3 declarations

      emDressedCompleted_returnem_dressed_prepared_sourceem_dressed_gt_prepared
29. L21Actual edge0 electronUnit=1; its independent-dual Noether current equals h_source and filtered current keeps the charge-commutator remainder.§9.3–9.5

    Actual edge0 electronUnit=1; its independent-dual Noether current equals h_source and filtered current keeps the charge-commutator remainder. The complete static residue C_T, finite pole/contact/complement Schur and C_T/(h_source*c_source) are generated; the source matching return is conditional on ordinaryFull-lightResponse=sourceCEM+contactResponse.

    Location: §9.3–9.5; §10.1; Appendix F.2✓ Kernel check passed

    Lean modules · 4

    • LowEnergyPhenomenology.AlphaSource.SourceElectronChargeUnit3 declarations

      sourceElectronChargeUnit_generatedsourceElectronIndependent_currentsourceElectronFiltered_current
    • LowEnergyPhenomenology.AlphaSource.SourceElectronStaticConsumer2 declarations

      sourceElectronStaticResidue_generatedsourceElectronStatic_rescale_invariant
    • LowEnergyPhenomenology.AlphaSource.SourceThomsonStaticResponse2 declarations

      sourceThomsonStaticInteraction_generatedsourceThomsonSchur_split
    • LowEnergyPhenomenology.AlphaSource.SourceThomsonMatchingConsumer2 declarations

      SourceThomsonMatchingContractsourceThomsonMatching_return
30. L19K*=(9023/9000)sqrt(30) is generated from the actual static inverse.§9.4

    K*=(9023/9000)sqrt(30) is generated from the actual static inverse. For independent preparations C_comp=K*w_D*w_S; their full original static residue contraction is -C_comp, while +kappa^2 times the all-direction complete interaction tends to +C_comp. The reduced scalar divides once by h_source*c_source(0).

    Location: §9.4; Appendix F.2✓ Kernel check passed

    Lean modules · 1

    • AlphaSource.EmIdentification.PhysicalEMCompleteStaticScalar4 declarations

      em_static_seed_generatedem_complete_static_residueem_complete_static_limitem_complete_static_reduced_limit
31. L23The repaired owner binds ordinaryFull in raw action units: ordinaryFull = (h_source*c_source)*beta*input.normalizedAmplitude = beta*input.amplitude, where beta is the source photon-left-reader of the same prepared covector.§9.5

    The repaired owner binds ordinaryFull in raw action units: ordinaryFull = (h_source*c_source)*beta*input.normalizedAmplitude = beta*input.amplitude, where beta is the source photon-left-reader of the same prepared covector. Keeping the original full-light/contact equation ordinaryFull-lightResponse=sourceCEM+contactResponse, the single (h_source*c_source)^-1 readout equals sourceCEM/(h_source*c_source). Conversion to the earlier matching consumer preserves the same values and equation; the full-light return consumes this owner.

    Location: §9.5✓ Kernel check passed

    Lean modules · 1

    • LowEnergyPhenomenology.AlphaSource.SourcePreparedThomsonMatchingBridge5 declarations

      SourcePreparedThomsonOwnerContractsourcePreparedThomsonOwner_prepared_fullsourcePreparedThomsonOwner_readoutSourcePreparedThomsonOwnerContract.toSourceThomsonContractsourcePreparedThomsonOwner_readout_as_matching
32. L25For the same actual edge0 electrons, the original whole ordinary photon response is N_D/(h_source*c_source(branch))*[beta_source(e)*D_D(polarization(e))-c_D(A_D(P_omega(e)J_source;lambda,T))], eventually on the original pole sheet.§9.5

    For the same actual edge0 electrons, the original whole ordinary photon response is N_D/(h_source*c_source(branch))*[beta_source(e)*D_D(polarization(e))-c_D(A_D(P_omega(e)J_source;lambda,T))], eventually on the original pole sheet. beta_source is the actual sourcePhotonLeftReader on the full source current and is not divided out. Both independent complex/real age windows and all original parameters remain.

    Location: §9.5; §10.5✓ Kernel check passed

    Lean modules · 1

    • AlphaSource.EmIdentification.PhysicalEMActualElectronOrdinary1 declarations

      actualElectronOrdinary_generated
33. §10Two-end returns of the actual electron: once-Coulomb and ordinary photon
34. L24The same actual charged edge0 rest leg (side,1) has native temporal expectation -1 and literal EM eigenvalue +1, using original actionScale*phaseMomentum=1.§10.1–10.4

    The same actual charged edge0 rest leg (side,1) has native temporal expectation -1 and literal EM eigenvalue +1, using original actionScale*phaseMomentum=1. The original once-Coulomb scalar is N_D[K*D_actual*W_cf-c_D(A_D(V_C))]. Both full 64-weight ends, complete static reader, oriented physicalTime/jointResolvent age windows, coframe false/true exchange and every single/cross leg correction are retained; separate source normalization produces the exact two-end correction formula.

    Location: §10.1–10.4; Appendix F.3✓ Kernel check passed

    Lean modules · 5

    • AlphaSource.EmIdentification.PhysicalNativeEMChargeBridge4 declarations

      sourceNativeElectronState_sourcenative_charged_current_unitem_reader_same_electron_stateem_filtered_electron_pair
    • AlphaSource.EmIdentification.PhysicalEMStaticReaderRecognition2 declarations

      em_static_reader_field_generatedem_static_reader_currentRestriction_generated
    • AlphaSource.EmIdentification.PhysicalEMActualStaticWindow2 declarations

      em_actual_origin_window_splitem_actual_origin_window_weighted
    • AlphaSource.EmIdentification.PhysicalEMActualCoulombScalar2 declarations

      em_staticCEM_scalar_generatedem_staticCEM_window_generated
    • AlphaSource.EmIdentification.PhysicalEMActualElectronCoulomb3 declarations

      coframeScalar_sameChargerawCEM_electron_generatedrawCEM_bothElectronLegs_generated
35. §11The original action identifies the scale of the electromagnetic carrier
36. L26The original E=−color2−Y/2 enters the four original gauge slots, and all 289 outputs/constraints are retained before EᵀG_wholeE and EᵀR E are generated.§11.1–11.3

    The original E=−color2−Y/2 enters the four original gauge slots, and all 289 outputs/constraints are retained before EᵀG_wholeE and EᵀR E are generated. The second variation of the genuine original repaired density at nativeLocalPoint is exactly the same K; the original carrier solves all 289 homogeneous equations, and the physical-frequency residue consumes K′ of the same action and returns its own flux. For any positive clock scale, the re-expressed actual Green function generates R_clock=Rω/scale at the moved pole, the actual Jacobi derivative is scale·K′, and the complete flux normalization identity is preserved; the original residue tensors on both sides scale together to 1/scale of their original values, and the R K′ projection is unchanged. The pole factor and visibility of the actual rest current are returned by the same source left reader; the two nonzero color derivatives of the original E background and all mixed rows are retained.

    Location: §11.1–11.3; Appendix G.1–G.2; Figure 4✓ Kernel check passed

    Lean modules · 3

    • AlphaSource.EmIdentification.ActualEMCarrier11 declarations

      emInsertionemPropagatingCarrieremPropagatoremPoleTensorem_pole_generatedem_carrier_homogeneousem_flux_generatedem_actual_background_derivativeem_electron_source_unitem_electron_native_factorem_electron_visibility_iff
    • AlphaSource.EmIdentification.ActualEMAction5 declarations

      em_action_sourceem_hessian_sourceem_jacobi_sourceem_action_carrier_homogeneousem_action_frequency_flux
    • AlphaSource.EmIdentification.ActualEMClock3 declarations

      em_clock_pole_generatedem_clock_jet_generatedem_clock_frequency_flux
37. §12The complete field Green function returns to Newton space
38. L27The same-source all-direction static operator-norm limit and the original Schwartz/Newton integrability bound generate a genuine Bochner matrix Fourier integral; the actual two-unit current keeps the 64 weights, all leg corrections, and the two independent windows, and the limiting coefficient is K·W_DW_S/(h c).§12.1–12.3

    The same-source all-direction static operator-norm limit and the original Schwartz/Newton integrability bound generate a genuine Bochner matrix Fourier integral; the actual two-unit current keeps the 64 weights, all leg corrections, and the two independent windows, and the limiting coefficient is K·W_DW_S/(h c). Joint scaling of profile/position/three-dimensional Jacobian gives degree −1, and the original Fourier integral contributes only one 4π. The two connected currents of the actual source-created unit minus background then enter the same whole289 integral with opposite transfers, and continuity generates by itself a common IR radius and domination bound; the limit is the original Newton convolution times −dot(F0ᵀJ_D(0),staticInverse(F0ᵀJ_S(0))), with the joint cross and return-return terms both present.

    Location: §12.1–12.3; Appendix G.3–G.5; Figure 5✓ Kernel check passed

    Lean modules · 3

    • AlphaSource.EmIdentification.ActualWholeCoulombPacket2 declarations

      actual_whole_coulomb_packet_originalactual_whole_coulomb_spatial_limit
    • AlphaSource.EmIdentification.ActualDressedFullCoulomb4 declarations

      dressed_current_originaldressed_current_continuousdressed_static_full_origindressed_coulomb_spatial_limit
    • AlphaSource.EmIdentification.ActualDressedMovingCoulomb3 declarations

      dressed_moving_static_uniformmoving_coulomb_packet_integrablemoving_coulomb_spatial_limit
39. §13Born overlaps become actual Coulomb dressing
40. L28Each complete N3 fullY/independent-sharp leg generates by itself a nonzero response and a unique norm-one normalization; the original bottom overlap=‖base‖/‖full response‖ lies strictly in (0,1], its square is exactly the original (3,0) unit Born value, and it is exactly 1 for a sharp leg.§13.1–13.3

    Each complete N3 fullY/independent-sharp leg generates by itself a nonzero response and a unique norm-one normalization; the original bottom overlap=‖base‖/‖full response‖ lies strictly in (0,1], its square is exactly the original (3,0) unit Born value, and it is exactly 1 for a sharp leg. When the detector pair and the source pair each have at least one independent sharp end, the product of the four actual overlaps times the original normalized base coefficient equals the complete Coulomb coefficient exactly; the norm of the difference is exactly (1−product) times the norm of the original base coefficient. It enters the original whole289 Newton spatial observation directly, with no externally supplied Z or matching scale.

    Location: §13.1–13.3; Appendix G.6; Figure 6✓ Kernel check passed

    Lean modules · 3

    • AlphaSource.EmIdentification.ActualCompositeFieldCurrent4 declarations

      composite_response_nonzerocomposite_unit_normcomposite_full_source_returncomposite_full_norm_four_legs
    • AlphaSource.EmIdentification.ActualCompositeGaugeBand4 declarations

      composite_response_bottomcomposite_weight_sharp_leftcomposite_weight_sharp_rightcomposite_output_charge_return
    • AlphaSource.EmIdentification.ActualCompositeCoulombDressing6 declarations

      composite_bottom_overlap_boundscomposite_bottom_born_readcomposite_sharp_bottom_overlapcomposite_coulomb_coefficient_dressingcomposite_coulomb_dressing_errorcomposite_coulomb_spatial_dressing