@@ -65,14 +65,12 @@ item to its proof.
6565 additive and multiplicative filtrations, including a constructive witness of
6666 their generic non-commutation.
6767
68- ** Realizability — corrected by its own formalization.** Which ultrametrics are
69- realizable by sibling-uniform radix laws (Theorem 43) was * mis-stated* in the
70- original specification: machine-checking produced a counterexample to the
71- stated conditions, an erratum in the spec (fdrs.md §6.6.1), and the corrected
72- full characterization — every open ball a prefix cylinder, plus canonical
73- cylinder diameters — proven in both directions
68+ ** Realizability.** The full characterization of which ultrametrics are
69+ realizable by sibling-uniform radix laws (Theorem 43): an ultrametric is
70+ realizable ** iff** every open ball is a prefix cylinder and every cylinder has
71+ canonical diameter — proven in both directions, with the two conditions doing
72+ provably separate work (the first pins the tree, the second pins the gauge)
7473([ ` MetricRealizability.lean ` ] ( FdrsFormal/Modes/VariableRadix/Realizability/MetricRealizability.lean ) ).
75- The repository treats this as the method working as intended.
7674
7775** Certified emission engines (Phase 13).** Continued-fraction timelines where
7876the gauge is generated rather than multiplied out, with Gosper-style
@@ -131,8 +129,8 @@ FdrsFormal/
131129├── Analysis/ # Digit-conditional signal analysis, the Fourier ceiling
132130├── Composition/ # Multi-timeline routing, deadlock-freedom, timing bounds
133131└── Modes/
134- ├── VariableRadix/ # Mode I, realizability (incl. the corrected Theorem 43),
135- │ # subshift gauges, the Gosper engine cluster
132+ ├── VariableRadix/ # Mode I, realizability (Theorem 43), subshift gauges ,
133+ │ # the Gosper engine cluster
136134 ├── ContextDependent/ # Mode II oracles
137135 ├── ExtendedBase/ # Mode III: walls, wires, the spatial thermometer
138136 ├── BaseZeroSea/ # Phase 10 substrate dynamics, the linear-chain bridge
0 commit comments