theorem proved term proof

`finite_phase_completeness`

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

formal statement (Lean)

  26theorem finite_phase_completeness (L : ReciprocalIntegerLedger) :
  27    ∃ c : ℕ, 0 < c ∧ Nonempty (ZMod c) := by

proof body

Term-mode proof.

  28  exact ⟨L.carrier, L.carrier_pos, ⟨0⟩⟩
  29
  30/-- A non-identity positive integer is separated from the identity in a finite
  31cyclic quotient.  We use the quotient `Z/(carrier+1)Z`: the carrier has phase
  32`-1`, not `1`. -/

depends on (23)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier_pos in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
carrier_pos in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
carrier_pos in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
ReciprocalIntegerLedger in IndisputableMonolith.NumberTheory.FinitePhaseCompleteness decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use