Measurement
Measurement modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Measurement |
0 | 4 | 2 | 93 | — |
Measurement.BornRule |
3 | 1 | 1 | 178 | — |
Measurement.BornRuleLight |
1 | 0 | 0 | 31 | — |
Measurement.C2ABridge |
5 | 0 | 1 | 225 | — |
Measurement.C2ABridgeLight |
1 | 0 | 0 | 27 | — |
Measurement.KernelMatch |
3 | 2 | 1 | 147 | — |
Measurement.PathAction |
1 | 1 | 3 | 55 | — |
Measurement.RSNative.Alignment |
0 | 0 | 3 | 55 | — |
Measurement.RSNative.Calibration.SI |
0 | 0 | 9 | 80 | — |
Measurement.RSNative.Calibration.SingleAnchor |
4 | 3 | 7 | 180 | — |
Measurement.RSNative.Core |
5 | 0 | 11 | 213 | — |
Measurement.RecognitionAngle.ActionSmallAngle |
4 | 0 | 4 | 93 | — |
Measurement.RecognitionAngle.AngleFunctionalEquation |
16 | 0 | 5 | 376 | — |
Measurement.RecognitionAngle.BlindCone |
2 | 0 | 1 | 42 | — |
Measurement.RecognitionAngle.TemporalGating |
2 | 0 | 4 | 76 | — |
Measurement.TwoBranchGeodesic |
3 | 1 | 5 | 91 | — |
Measurement.WindowNeutrality |
3 | 0 | 1 | 59 | — |