theorem proved term proof

`bits_bijection`

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

formal statement (Lean)

  67theorem bits_bijection (t : TickIndex) : bitsToTick (tickToBits t) = t := by

proof body

Term-mode proof.

  68  simp [tickToBits, bitsToTick]
  69  ext
  70  simp
  71  omega
  72
  73/-! ## Generation from Dimensional Parity -/
  74
  75/-- A generation is characterized by the parity pattern across dimensions.
  76    We define 3 "generation modes" from the bit patterns. -/

depends on (18)

Lean names referenced from this declaration's body.

modes in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
Generation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Generation in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Generation in IndisputableMonolith.Physics.CKM decl_use
bitsToTick in IndisputableMonolith.Physics.ThreeGenerations decl_use
Generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
TickIndex in IndisputableMonolith.Physics.ThreeGenerations decl_use
tickToBits in IndisputableMonolith.Physics.ThreeGenerations decl_use
Generation in IndisputableMonolith.RecogSpec.RSLedger decl_use