IndisputableMonolith.Quantum

   1import IndisputableMonolith.Quantum.RecognitionFirst.EightTickWeyl
   2import IndisputableMonolith.Quantum.PureTwoQubit.EntropyConcurrence
   3import IndisputableMonolith.Quantum.HolographicBound
   4import IndisputableMonolith.Quantum.BornRule
   5
   6/-!
   7# IndisputableMonolith.Quantum
   8
   9Quantum module facade — re-exports the public quantum-layer formalizations that
  10derive standard quantum structure from the recognition substrate:
  11
  12- `Quantum.RecognitionFirst.EightTickWeyl`: the finite Heisenberg–Weyl relation on
  13  the 8-tick recognition cycle `ZMod 8`. `clock ∘ shift = ω • (shift ∘ clock)` with
  14  `ω` a primitive 8th root of unity (`eightTick_weyl`), so occupation and cost-rate do
  15  not commute (`canonical_noncommutativity`). This is the recognition root of the
  16  canonical commutator `[x,p] ≠ 0`; the continuum limit `[x,p] = iℏ` and the magnitude
  17  `ℏ = φ⁻⁵` are OPEN, not asserted here. Axiom-clean.
  18
  19- `Quantum.PureTwoQubit.EntropyConcurrence`: the Wootters `concurrence` of a pure
  20  two-qubit amplitude matrix and its entanglement entropy. `concurrence_nonneg`,
  21  `concurrence_eq_zero_iff_det_zero`, the binary entropy `h(p)`, and the certificate
  22  `PureTwoQubitConcurrenceEntropyCert` linking positive concurrence to positive entropy.
  23
  24- `Quantum.HolographicBound`: the holographic bound `S ≤ A/(4 l_P²)` (`holographic_bound`),
  25  its derivation from ledger projection (`holography_from_ledger`), the Bekenstein bound,
  26  and the area-scaling of information.
  27
  28- `Quantum.BornRule`: the Born rule from the recognition cost functional. The
  29  measurement weight `r ↦ r²` is forced by the two-branch geodesic action and the
  30  kernel-match certificate (`born_rule_from_jcost`), and `gleason_from_rs` packages the
  31  Gleason-style derivation from the recognition substrate. Its dependency base is the
  32  neutral `Spectral.DFT8` backbone and the `Foundation.ComplexStructureForcing` /
  33  `Foundation.BornRuleForcing` chain, all Mathlib-only and axiom-clean. This replaces the
  34  earlier note that the Born-rule derivation remained private: its measurement
  35  certificates (`Measurement.PathAction`, `TwoBranchGeodesic`, `KernelMatch`, `C2ABridge`,
  36  `Verification.TwoOutcomeBornCert`) have been refactored onto the clean substrate.
  37
  38These export no later-physics or private application verticals.
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Quantum
  43
  44end Quantum
  45end IndisputableMonolith
  46