IndisputableMonolith
IndisputableMonolith.lean · 85 lines · 0 declarations
show as:
view math explainer →
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