gap — Recognition explainer

formal statement (Lean)

 100def gap : ℕ := closure_factor * fibonacci_factor

proof body

Definition body.

 101
 102/-- **Main Theorem**: The gap equals 45. -/

used by (40)

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

Jphi_numerical_band in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
visualBeautyCert in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
adjacencyGap_eq in IndisputableMonolith.Archaeology.PotterySerialFromJCost decl_use
adjacencyGap_pos in IndisputableMonolith.Archaeology.PotterySerialFromJCost decl_use
popularity_le_one in IndisputableMonolith.Archaeology.PotterySerialFromJCost decl_use
potterySerialCert in IndisputableMonolith.Archaeology.PotterySerialFromJCost decl_use
averageGap_eq in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
averageGap_in_gap45_band in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
styleGap in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
styleSuccessionCert in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
westernCanon_length in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
BIT_carrier_period_band in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
fastRadioBurstFromBITCert in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
FRB_period_strict_increasing in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
planetaryFormationCert in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
r_orbit_gap_skip_band in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
bimodal_ratio_lt_phi_nine in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
gap_size_pos in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
pulsarPeriodFromRungCert in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
pulsar_period_one_statement in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
forecastSkill_decay in IndisputableMonolith.Climate.ClimateForecastSkillFromJCost decl_use
lorenzLimitDays in IndisputableMonolith.Climate.ClimateForecastSkillFromJCost decl_use
sat_recognition_time in IndisputableMonolith.Complexity.CellularAutomata decl_use
CircuitLedgerCert in IndisputableMonolith.Complexity.CircuitLedger decl_use
circuitSeparation in IndisputableMonolith.Complexity.CircuitLedger decl_use
no_sublinear_universal_decoder in IndisputableMonolith.Complexity.CircuitLedger decl_use
SpectralTuringBridgeHypothesis in IndisputableMonolith.Complexity.CircuitLedger decl_use
RecognitionScenario in IndisputableMonolith.Complexity.ComputationBridge decl_use
empty_formula_flat_landscape in IndisputableMonolith.Complexity.SpectralGap decl_use

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.

closure_factor in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use