IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PhysicalOneActCalibration

   1/-
   2  PrimitiveRecognitionCalculus/PhysicalOneActCalibration.lean
   3
   4  Physical instrument wrapper for the one-act calibration datum.
   5
   6  `DeltaRealCalibration.lean` proves the mathematical classification: the
   7  residual cost unit is a faithful one-real torsor, and the normalized one-act
   8  curvature datum forces the canonical unit. This file names the corresponding
   9  physical interface: an instrument whose readout is calibrated to the primitive
  10  one-act curvature and whose lock value is one.
  11
  12  This does not pretend the instrument is built in Lean. It proves the exact
  13  logical role of such an instrument: if it reads the one-act curvature and its
  14  locked readout is `1`, then it produces the normalized interface and forces
  15  the canonical cost unit.
  16
  17  No project-local axioms. No sorry.
  18-/
  19
  20import Mathlib
  21import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration
  22
  23namespace IndisputableMonolith
  24namespace Foundation
  25namespace PrimitiveRecognitionCalculus
  26namespace PhysicalOneActCalibration
  27
  28open DeltaRealCalibration
  29
  30/-- A physical one-act instrument: a positive candidate unit, a real readout, a
  31proof that the readout is exactly the one-act curvature of that unit, and a lock
  32showing the readout equals one. -/
  33structure OneActInstrument where
  34  unit : ℝ
  35  positive : 0 < unit
  36  readout : ℝ
  37  reads_curvature : readout = oneActCurvature unit
  38  locked_to_one : readout = 1
  39
  40/-- A one-act instrument supplies the normalized continuum-side interface. -/
  41def OneActInstrument.toInterface (I : OneActInstrument) : NormalizedOneActInterface where
  42  unit := I.unit
  43  positive := I.positive
  44  curvature_unit := by
  45    rw [← I.reads_curvature, I.locked_to_one]
  46
  47/-- The physical one-act instrument forces the canonical cost unit. -/
  48theorem instrument_forces_canonical_unit (I : OneActInstrument) :
  49    I.unit = 1 :=
  50  normalized_interface_forces_J I.toInterface
  51
  52/-- The canonical instrument exists at the canonical unit. This is a consistency
  53witness, not a construction of lab hardware. -/
  54def canonicalInstrument : OneActInstrument where
  55  unit := 1
  56  positive := by norm_num
  57  readout := 1
  58  reads_curvature := by
  59    rw [oneActCurvature_eq]
  60    norm_num
  61  locked_to_one := rfl
  62
  63/-- **Physical calibration headline.** The abstract one-act normalization is
  64exactly the datum supplied by a physical one-act instrument: any such instrument
  65produces the normalized interface and forces `unit = 1`, and the canonical unit
  66carries a consistent instrument witness. -/
  67theorem physical_one_act_calibration_headline :
  68    (∀ I : OneActInstrument, I.unit = 1)
  69      ∧ (∃ I : OneActInstrument, I.unit = 1)
  70      ∧ (∀ I : OneActInstrument, (OneActInstrument.toInterface I).unit = I.unit) :=
  71  ⟨instrument_forces_canonical_unit, ⟨canonicalInstrument, rfl⟩, fun _ => rfl⟩
  72
  73end PhysicalOneActCalibration
  74end PrimitiveRecognitionCalculus
  75end Foundation
  76end IndisputableMonolith
  77