IndisputableMonolith.Gravity.SevenGaps.HorizonLedgerPreflight

declarations in this module (33)

• theorem below L121
• def schwarzschildHorizonAreaMirror L151
• theorem horizonAreaMirror_scaling L157
• theorem horizonAreaMirror_scaling_admissible L168
• theorem ledgerCapacityMirror_scaling L176
• theorem horizonArea_achieves_every_positive L183
• theorem scaling_family_blocks_ledger_gap L200
• def scaleLedger L228
• theorem scaleLedger_boundaryCost L248
• theorem ledger_boundary_cost_no_uniform_gap L260
• structure HorizonPatchClassTarget L303
• def fibPatchWitness L317
• theorem fib_ratio_tendsto_phi L336
• theorem log_fib_gap_tendsto_log_phi L345
• structure HorizonCombModel L378
• def entropy L392
• def area L398
• theorem entropy_gap_tendsto L403
• theorem area_gap_tendsto L417
• def horizonCombModelWitness L429
• def AreaGapTarget L440
• def combFrequencyGM L454
• theorem combFrequencyGM_pos L456
• theorem combFrequencyGM_bounds L467
• def kerrCombOffset L488
• theorem kerrCombOffset_eq L493
• def modelTransitionFrequency L505
• theorem model_area_gap_gives_kerr_comb L511
• theorem schwarzschild_comb_frequency L523
• def AdjacentSectorTransitionNonzero L540
• structure HorizonCombPreflightStatus L550
• def horizonCombPreflightStatus L570
• theorem horizonCombPreflightStatus_flags L581