theorem proved term proof

`embed_pos`

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

formal statement (Lean)

 566theorem embed_pos (γ : Generator) (n : LogicNat) : 0 < embed γ n := by

proof body

Term-mode proof.

 567  induction n with
 568  | identity => exact one_pos
 569  | step n ih =>
 570    show 0 < γ.value * embed γ n
 571    exact mul_pos γ.pos ih
 572
 573/-- **Multiplicative homomorphism**: addition in `LogicNat` corresponds
 574to multiplication of orbit elements. This is the structural fact that
 575`LogicNat` *is* the orbit, parameterized by iteration count. -/

depends on (18)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
step in IndisputableMonolith.Complexity.CellularAutomata decl_use
embed in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
Generator in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
embed in IndisputableMonolith.Foundation.HamiltonianEmergence decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing 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
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use