lemma proved term proof

`path_action_single`

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

formal statement (Lean)

 137lemma path_action_single (c : Config) : PathAction [c] = J c.value := rfl

proof body

Term-mode proof.

 138
 139/-- **PATH WEIGHT**: The exponential weight of a path.
 140
 141    W[γ] = exp(-C[γ])
 142
 143    This is the fundamental quantity that gives rise to the Born rule. -/

depends on (17)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers 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
Config in IndisputableMonolith.Gravity.ILG decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
PathAction in IndisputableMonolith.Modal.Actualization decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use