theorem proved term proof

`atmospheric_correction_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  96theorem atmospheric_correction_eq : atmospheric_correction = 6 * alpha := by

proof body

Term-mode proof.

  97  unfold atmospheric_correction atmospheric_coefficient
  98  rfl
  99
 100/-! ## Derivation of the Coefficient 10 (Solar) -/
 101
 102/-- The solar correction coefficient is edges minus the active pair.
 103
 104    **Physical interpretation**: The solar sector involves 2-step torsion
 105    (φ⁻² weight), coupling via edges. The 12 edges minus the 2 active
 106    modes (e and ν_e in the 1-2 sector) gives 10 passive contributions. -/

depends on (18)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
modes in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
step in IndisputableMonolith.Complexity.CellularAutomata decl_use
alpha in IndisputableMonolith.Constants.Alpha decl_use
via in IndisputableMonolith.Derivations.MassToLight decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
atmospheric_coefficient in IndisputableMonolith.Physics.PMNSCorrections decl_use
atmospheric_correction in IndisputableMonolith.Physics.PMNSCorrections decl_use