Phase — Recognition explainer

formal statement (Lean)

  46abbrev Phase := Fin 8

proof body

Definition body.

  47
  48/-- The number of phases in one 8-tick cycle. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

sc_gap_scale in IndisputableMonolith.CondensedMatter.JCostPhaseTransition decl_use
J_bit in IndisputableMonolith.Constants decl_use
ticksToOctaves in IndisputableMonolith.Constants.RSNativeUnits decl_use
PhaseLocked in IndisputableMonolith.Cosmology.DarkEnergyEOS decl_use
mondStatus in IndisputableMonolith.Cosmology.DarkMatter decl_use
VoxelSymmetric in IndisputableMonolith.Cosmology.VacuumUniformity decl_use
dAlembert_contDiff_smooth in IndisputableMonolith.Cost.AczelProof decl_use
dAlembert_to_ODE_general in IndisputableMonolith.Cost.AczelProof decl_use
smooth in IndisputableMonolith.Cost.AczelProof decl_use
octavePhase in IndisputableMonolith.Cost.Ndim.Octave decl_use
SignFlipFalsifier in IndisputableMonolith.Flight.Falsifiers decl_use
fundamentalFrequency in IndisputableMonolith.Foundation.EightTick decl_use
isOddTick in IndisputableMonolith.Foundation.EightTick decl_use
phase_4_is_minus_one in IndisputableMonolith.Foundation.EightTick decl_use
phase_eighth_power_is_one in IndisputableMonolith.Foundation.EightTick decl_use
uniform_scaling_forced in IndisputableMonolith.Foundation.HierarchyForcing decl_use
LogicComplexAnalyticSubstrateCert in IndisputableMonolith.Foundation.LogicComplexCompat decl_use
born_rule_jcost_connection in IndisputableMonolith.Foundation.QuantumLedger decl_use
LedgerEntry in IndisputableMonolith.Foundation.QuantumLedger decl_use
calibrated_iff_hypothesis in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use
field_curvature_identity_simplicial in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use
field_curvature_identity_simplicial_einstein in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use
simplicial_linearization_discharge in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use
selfAware_max_richness in IndisputableMonolith.Foundation.VoiceForcing decl_use
closure_number_eq_9 in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
dimension_forcing in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
regular_not_flat in IndisputableMonolith.Geometry.CayleyMenger decl_use
linearizedDeficit in IndisputableMonolith.Geometry.DeficitLinearization decl_use
totalDeficit_flat in IndisputableMonolith.Geometry.Schlaefli decl_use
forcing_chain_complete in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use

… and 10 more

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
Phase in IndisputableMonolith.RRF.Hypotheses.EightTick decl_use