Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PhysicalOneActCalibration

show as:
view Lean formalization →

Defines a physical one-act instrument: a positive candidate unit together with a real readout forced to equal the one-act curvature of that unit and locked to the value one. Anyone calibrating the native recognition unit from a single act cites this package. The argument packages the unit, the readout identity, and the unit-lock into one structure and shows that any such instrument is forced onto the canonical scale.

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$ onto the canonical unit; the module supplies the canonical instrument and a headline calibration theorem.

background

Recognition Science measures cost via the J-functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), unique under the Recognition Composition Law. Primitive recognition calculus works one act at a time: a single recognition step produces a curvature (defect) that must be read out in physical units.

This module sits on top of DeltaRealCalibration, which already ties real-valued delta readouts to the recognition cost. The local objects are a candidate positive unit, a real scalar readout of one-act curvature on that unit, and a lock that the readout equals one. The point is to turn an abstract curvature identity into a physical calibration statement: if an instrument truly measures one act and reports one, its unit cannot float.

Sibling names in the module mark the structure (OneActInstrument), the forcing lemma that any such instrument is canonical, the canonical instrument itself, and a headline theorem packaging the calibration.

proof idea

Definition-plus-forcing module rather than a long derivation. It introduces the instrument bundle (positive unit, real readout, curvature identity, lock to one), then proves that any instrument satisfying those data is forced onto the canonical unit. The canonical instrument is exhibited as a witness, and a short headline theorem restates the calibration conclusion for downstream import. Upstream real-calibration facts from DeltaRealCalibration supply the curvature-to-readout bridge; the new work is the packaging and the unit-forcing step.

why it matters in Recognition Science

Native delta analysis and strong closure both import this module. Without a physical one-act lock, later native-scale theorems would still carry a free unit choice. The instrument forces that choice: readout equals one-act curvature and equals one, so the unit is canonical.

In the broader forcing chain this is calibration infrastructure under the J-uniqueness and self-similar fixed-point steps (T5–T6): once J is fixed and $\phi$ is the self-similar scale, a one-act instrument must sit on that scale. Downstream DeltaNativeAnalysis and DeltaNativeStrongClosure can therefore treat the native unit as already pinned rather than hypothesized.

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)