escape
plain-language theorem explainer
The escape definition supplies a minimal string operation that replaces each double-quote character with its escaped form. It is called by the sibling quote helper to embed field values safely inside the deterministic JSON audit report of unitless invariants. The body consists of a single replace call with no further logic or recursion.
Claim. Define the map escape : String → String by replacing every occurrence of the character $``$ in the input string $s$ with the two-character sequence $``$
background
The Audit module supplies scaffolding for milestone M1: a deterministic JSON summary of already-proven unitless invariants drawn from the Recognition framework. The module doc states that this surface will later be extended to numeric values and scale-declared running quantities. The escape helper is required to embed string fields without breaking JSON syntax.
proof idea
One-line definition that applies the built-in string replace operation to the input s, substituting the double-quote character with its escaped counterpart.
why it matters
The definition is required by the quote helper and therefore by audit_json_report and runAudit, which emit summaries of the forcing chain (T0–T8), the Recognition Composition Law, and the phi-ladder constants. It is referenced by downstream results including continuous_no_isolated_zero_defect, phiHierarchy_unique, identity_always_possible, and arrowOfTime. The module positions the whole audit surface as a placeholder that will be extended once numeric scale-declared quantities are available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.