theorem proved term proof

`RSReal_gen_phi_one`

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

formal statement (Lean)

 505theorem RSReal_gen_phi_one : RSReal_gen phi_ladder 1 :=

proof body

Term-mode proof.

 506  RSReal_gen_at_one one_mem_phi_ladder
 507
 508/-! ## Numeric Verification of Paper Examples (Section 4.1)
 509
 510The paper uses concrete J-cost values in Tables 1–3.
 511We verify each value used.
 512-/
 513

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
phi_ladder in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
one_mem_phi_ladder in IndisputableMonolith.Foundation.OntologyPredicates decl_use
phi_ladder in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSReal_gen in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSReal_gen_at_one in IndisputableMonolith.Foundation.OntologyPredicates decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
phi_ladder in IndisputableMonolith.Foundation.StillnessGenerative decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use