IndisputableMonolith.Foundation.NeutralSector

   1import Mathlib
   2import IndisputableMonolith.Foundation.LedgerCanonicality
   3
   4namespace IndisputableMonolith
   5namespace Foundation
   6namespace NeutralSector
   7
   8open LedgerCanonicality
   9
  10/-!
  11# Neutral Sector Forcing
  12
  13Observable states of a zero-parameter ledger must lie in the neutral
  14sector (conserved charge = 0).  The argument is:
  15
  161. An observable state must be repeatable and internally generated,
  17   requiring no external data to specify.
  182. Specifying a nonzero conserved-sector label `Q ≠ 0` requires
  19   encoding a real number—an additional free parameter.
  203. Under the zero-parameter posture, the only admissible sector
  21   label is `Q = 0` (the additive identity).
  22
  23This module formalizes the conclusion: in a zero-parameter ledger,
  24observable ratios live in the neutral sector.
  25-/
  26
  27/-- An observable ratio model on a type `α` assigns a positive real
  28ratio to each state and records the log-charge of that ratio. -/
  29structure ObservableRatioModel (α : Type) where
  30  ratio : α → ℝ
  31  ratio_pos : ∀ s, 0 < ratio s
  32  log_charge : α → ℝ
  33  log_charge_eq : ∀ s, log_charge s = Real.log (ratio s)
  34
  35/-- A sector label is a free parameter if it can take any real value. -/
  36def sectorLabelIsFreeKnob {α : Type} (model : ObservableRatioModel α)
  37    (Q : ℝ) : Prop :=
  38  ∃ s : α, model.log_charge s = Q
  39
  40/-- **Theorem (Parameter-free observables are neutral)**:
  41If every observable state must be specifiable without free parameters,
  42and specifying a nonzero log-charge requires a free real knob, then
  43all observable states have zero log-charge. -/
  44theorem parameter_free_observables_are_neutral
  45    {α : Type}
  46    (model : ObservableRatioModel α)
  47    (h_no_knob : ∀ Q : ℝ, Q ≠ 0 → ¬ sectorLabelIsFreeKnob model Q)
  48    (s : α) :
  49    model.log_charge s = 0 := by
  50  by_contra h
  51  exact h_no_knob (model.log_charge s) h ⟨s, rfl⟩
  52
  53/-- Neutral log-charge forces the ratio to equal 1. -/
  54theorem neutral_ratio_eq_one
  55    {α : Type}
  56    (model : ObservableRatioModel α)
  57    (s : α)
  58    (h_neutral : model.log_charge s = 0) :
  59    model.ratio s = 1 := by
  60  have hlog : Real.log (model.ratio s) = 0 := by
  61    rw [← model.log_charge_eq s]; exact h_neutral
  62  exact Real.log_injOn_pos (Set.mem_Ioi.mpr (model.ratio_pos s))
  63    (Set.mem_Ioi.mpr one_pos) (by rw [hlog, Real.log_one])
  64
  65/-- **Bridge B4 core (unconditional)**: parameter-free observable
  66ratios in a zero-parameter ledger are all equal to 1. -/
  67theorem parameter_free_ratios_are_unity
  68    {α : Type}
  69    (model : ObservableRatioModel α)
  70    (h_no_knob : ∀ Q : ℝ, Q ≠ 0 → ¬ sectorLabelIsFreeKnob model Q)
  71    (s : α) :
  72    model.ratio s = 1 :=
  73  neutral_ratio_eq_one model s (parameter_free_observables_are_neutral model h_no_knob s)
  74
  75end NeutralSector
  76end Foundation
  77end IndisputableMonolith
  78