Pith. sign in

IndisputableMonolith

IndisputableMonolith.lean · 85 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending · generated 2026-07-07 08:06:24.587822+00:00

   1import IndisputableMonolith.Foundation.NothingToDistinction
   2import IndisputableMonolith.Foundation.TMinus1ToT8Bridge
   3import IndisputableMonolith.RecognitionCore
   4import IndisputableMonolith.LedgerFloor
   5import IndisputableMonolith.Gravity
   6import IndisputableMonolith.Foundation.MeasureForcing
   7import IndisputableMonolith.Constants.AlphaGenesis
   8import IndisputableMonolith.Quantum
   9
  10/-!
  11# Shape of Logic — root module
  12
  13Public root for the core Shape of Logic release. This repository exports the
  14core theory of `/reality`: the T-2 through T8 theorem spine, the recognition
  15geometry that carries observable content, and the core gravity (ILG) layer. It
  16exports no later-physics or private application verticals; those remain in the
  17`/reality` repository.
  18
  19## Forcing-chain spine
  20
  21* `NothingToDistinction.nothingToDistinctionCert`
  22* `TMinus1ToT8Bridge.complete_forcing_chain_tminus2_to_t8`
  23* `CircleWindingChain.circleH1ZNonzero_unconditional`
  24* `CircleWindingChain.circleH1ZIsoInt_holds`
  25
  26## Recognition core (T0 / T4 layer)
  27
  28* `RecognitionCore.forced_quotient_iff`
  29* `RecognitionCore.signature_complete_iff_separating`
  30* `RecognitionCore.one_bit_not_complete_boundary`
  31* `RecognitionCore.recognizer_refinement`
  32
  33## Ledger floor (Boolean shadow of the extensive recognition ledger)
  34
  35* `LedgerFloor.DefectLedger`
  36* `LedgerFloor.ledger_floor_t0_bridge`
  37* `LedgerFloor.ledger_t0_identification_certificate`
  38* `LedgerFloor.two_independent_same_defects`
  39
  40## Core gravity (ILG)
  41
  42* `Gravity.ILG` — information-limited-gravity time-kernel and weight functions
  43* `Gravity.Rotation` — Newtonian rotation-curve identities
  44
  45## Forced measure (T9) and Alpha Genesis
  46
  47* `Foundation.MeasureForcing.t9_measure_forced` — the recognition measure
  48  `w(n) = φ⁻ⁿ` is forced (lattice + continuum layers, Gibbs form,
  49  partition function `Z = φ²`)
  50* `Constants.AlphaGenesis.DressingResponse.response_forced` — the
  51  exponential dressing of the α seed is forced (factorization + unit
  52  response); the additive form is excluded
  53* `Constants.AlphaGenesis.EightTickLadder.pattern_forced` — the φ-pattern
  54  on the 8-tick carrier is forced by T6 self-similarity
  55* `Constants.AlphaGenesis.alphaInv_eq_seed_mul_forced_weight` —
  56  `α⁻¹ = (4π·11) · contWeight(w₈/(4π·11))`: the dressing shape is the forced
  57  measure at the spectral gap load. HONEST STATUS: the seed `4π·11` is an
  58  identification, not a derived coupling, and the first-order value is
  59  excluded by measurement (see `MeasurementVerdict` below); exact `α⁻¹(0)`
  60  is a boundary condition, OPEN
  61* `Constants.AlphaGenesis.AlphaGenesisCert.verified_any` — the seven-clause
  62  forward-derivation certificate (M1–M3 reference no measured value)
  63* `Constants.AlphaGenesis.existsUnique_closingLoad` — the second-order
  64  residual problem has exactly one answer in load units (quarantine module)
  65* `Constants.AlphaGenesis.MeasurementVerdict.alphaInvGenesis_exceeds_CODATA_by_0007`
  66  — the measurement verdict: the first-order construction value exceeds
  67  CODATA by more than `7×10⁻⁴`, an exclusion at more than 30,000σ
  68  (`margin_0007_gt_30000_sigma`)
  69* `Constants.AlphaGenesis.KappaGamma.alpha_not_pinned_by_forcedClosure` and
  70  `kappa_blind_closure_cannot_pin` — the irreducibility theorems: the forced
  71  closure is κ_γ-independent and no normalization-blind condition can pin
  72  the coupling, so within RS the exact value of `α⁻¹` is a free boundary
  73  datum (the U(1) kinetic normalization), not a derived constant
  74* `Gravity.DerivedFactors` — HSB suppression from SevenBeatViolation saturation
  75
  76## Quantum layer (recognition-first)
  77
  78* `Quantum.RecognitionFirst.eightTick_weyl` — the finite Heisenberg–Weyl relation on
  79  the 8-tick recognition cycle; `canonical_noncommutativity` is the recognition root of
  80  `[x,p] ≠ 0` (continuum `[x,p]=iℏ` and `ℏ=φ⁻⁵` remain OPEN)
  81* `Quantum.PureTwoQubit.EntropyConcurrence` — Wootters concurrence and the
  82  concurrence→entropy certificate for pure two-qubit states
  83* `Quantum.HolographicBound.holographic_bound` — `S ≤ A/(4 l_P²)` from ledger projection
  84-/
  85

source mirrored from github.com/jonwashburn/shape-of-logic