Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PhysicalOneActCalibration

show as:
view Lean formalization →

Physical one-act calibration packages a positive candidate unit with a real readout equal to that unit's one-act curvature and locked to one. Researchers fixing the RS unit scale from a single recognition act cite this module. It defines the instrument structure, proves any such instrument forces the canonical unit, and records a headline calibration theorem for native-delta work.

claimA physical one-act instrument is a positive candidate unit $u>0$, a real readout $r$, a proof that $r$ equals the one-act curvature of $u$, and a lock $r=1$. Any such instrument forces $u$ to the canonical calibrated unit. The module exhibits a canonical instrument and a headline one-act calibration theorem.

background

In Recognition Science the primitive recognition calculus measures curvature of candidate units against the cost structure forced by the Recognition Composition Law. Upstream, DeltaRealCalibration supplies the real-valued calibration of the one-act defect against which physical instruments are judged.

This module sits in Foundation.PrimitiveRecognitionCalculus. A one-act instrument is the operational package: choose a positive scale, obtain a real readout, certify that the readout is exactly the one-act curvature of that scale, and require the readout to equal one. The lock $r=1$ is the physical statement that a single recognition act has been normalized to unit curvature.

Sibling content includes the instrument structure, the forcing lemma that any instrument selects the canonical unit, a canonical instrument construction, and a headline calibration theorem.

proof idea

Definition-first module with short forcing proofs. It introduces the one-act instrument structure bundling unit, readout, curvature identity, and unit lock. The forcing result reduces the lock plus curvature identity to uniqueness of the calibrated unit inherited from DeltaRealCalibration. A canonical instrument is witnessed by the already-calibrated unit with readout one. The headline theorem packages structure, forcing, and witness for downstream native-delta analysis.

why it matters in Recognition Science

Downstream modules DeltaNativeAnalysis and DeltaNativeStrongClosure import this calibration so the native one-act defect can be treated on a fixed physical scale. Without locking the readout to one and forcing the unit, native analysis would retain an arbitrary positive scale factor. In the RS foundation stack this is the bridge from real-valued delta calibration to the dimensionless native calculus used later in forcing and ladder work. It does not itself run T5--T8, but supplies the unit convention those steps assume when speaking of physical one-act curvature.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)