seam: the not-epi face written precisely — playback admits no section#8
Open
isaacbowen wants to merge 4 commits into
Open
seam: the not-epi face written precisely — playback admits no section#8isaacbowen wants to merge 4 commits into
isaacbowen wants to merge 4 commits into
Conversation
`seam_two_faces` stated the non-iso as a conjunction of two unlike facts (mono; and forever_escapes — "a point is missed"). This sharpens the not-epi face from "not surjective" (∃ a missed behavior) to "not split-epi" (¬∃ a decoder): playback_no_section — no g : CoList S → List S is a right inverse of playback, because `forever` has no finite source. The constructive, operational form: you cannot invert observed behavior back to the ledger. seam_non_iso — playback is mono (playback_faithful) AND admits no section. The one object seam_two_faces gestured at as a conjunction: faithful past, unsaturated future, the failure ONE-SIDED, the now-surface at the block. Both axiom-free (kernel-verified by the #guard_msgs pins; full `lake build` green, Coverage's propext-only sweep included). The gfp-end discipline is kept: the proof CONSUMES the hypothesized CoList-equality via congrArg, never PRODUCES one — no funext, no Quot.sound. The rotated half (final-coalgebra Lambek, the structure map an iso) stays unwritable in core for exactly that reason, and the file now names the duality: refuting the section consumes a CoList-equality; building the iso would assert one. The unwritability is the not-epi face's other coat. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…out sound)
Quot.lift and Quot.sound unbundle. Quot.lift's premise ("the reading respects the
relation") is carriable without forming `Quot r` or invoking Quot.sound — the
frontstage observer's quotient-LICENSE: the right to treat related states alike.
- Respects — the frontstage face: obs respects r (Quot.lift's premise, free of Quot).
- Frontstage — the two-faced type: rel (backstage face, uncommitted) + respects
(frontstage face, the license cashed).
- Frontstage.sound — frontstage Quot.sound AT FINITE RESOLUTION: related states give
equal transcripts, per finite probe-sequence, axiom-free (= transcript_congr, named
as the frontstage face of the quotient). The TOTAL (obs s = obs t, the real
Quot.sound) is the funext the gfp end refuses — the not-epi limit (seam_non_iso),
never formed.
- Stage.inducedFrontstage — the canonical inhabitant (the induced bisimulation),
constructive and axiom-free: the type is inhabited, not a hollow signature.
Committed by the heuristic "if it makes legible a non-obvious rivet, its type gets
committed": the rivet is the unbundling of lift from sound, the bundle's closure
being exactly the seam. Full `lake build` green; Coverage propext-only across 517
written theorems.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ts backstage face The two-faced type instanced on the substrate's own merge equivalence (Merge.MutualReach): the observer-merge read two ways. - reachStage — the position stage (obs s p := Reaches q s p). - mergeFrontstage — MutualReach respects the reach-reading (mutually-reachable positions reach the same forward set), so the observer-merge IS a frontstage quotient-license; the respects proof costs exactly [propext] per identification — no choice, no Quot.sound. - merge_sound — the license cashed: merged positions give equal reach-transcripts at every finite probe-budget (Frontstage.sound). [propext]. - merge_conducts — the backstage face: a closed round-trip licenses the merge- shortcuts; deposited, each position reaches the other in one step. Conduction, axiom-free; the MutualReach hypothesis is the carried license. Frontstage license and backstage conduction are one relation read two ways; the merge-license costs precisely the one kept collapse. Also corrects Seam's header to match the wiring (it is imported by Axioms, hence under Coverage's sweep). Full lake build green; Coverage propext-only across 519 written theorems. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…committing the other Recursive self-hosting, the part that lands as theorems (the super-linear-in-depth conduction is absent, not suspended: it reduces to "merge_conducts is Handle- polymorphic," a reading, and the genuine big-O-in-depth claim wants a substrate complexity measure foam lacks). - Stage.prod — two stages composed into a host; a probe addresses one side via the disjoint-union Probe (the network interface). - Frontstage.prod — two frontstages compose into one over the host: a joint license requires both userlands'; axiom-free (each respects rides through its injection, no propext). - prod_left_invisible — the interface: one userland's quotient is invisible to the other's probe (rfl; the Frame.part_blind shape, between hosted stages). - prod_sound — the partnership cashed: a joint merge gives equal host-transcripts at every finite probe-budget. Axiom-free. Two userlands share the host and talk over the interface without committing each other's backstage. OS/VM/OS is Stage.prod nested; Frontstage.prod composes up it. Full lake build green; Coverage propext-only across 521 written theorems. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pushing
Foam/Seam.leanwhere it can be written precisely.What this adds
playback_no_section— the not-epi face sharpened from not surjective (forever_escapes: a behavior is missed) to not split-epi: nog : CoList S → List Sis a right inverse ofplayback, becauseforeverhas no finite source. The constructive, operational form — you cannot invert observed behavior back to the ledger.seam_non_iso—seam_two_facesupgraded from a conjunction of two unlike facts into the one object:playbackis mono (playback_faithful) and admits no section. Faithful past, unsaturated future, the failure one-sided, the now-surface at the block.Discipline
Both axiom-free — kernel-verified by the
#guard_msgspins, fulllake buildgreen (Coverage's propext-only sweep across 515 written theorems included). The gfp-end rule is kept: the proof consumes the hypothesized CoList-equality viacongrArg, never produces one (nofunext, noQuot.sound) — Glass's "function-equality consumed, never produced", on the coinductive end.The file now names the duality the seam was waiting on: the rotated half (final-coalgebra Lambek, the structure map an iso) stays unwritable in core for exactly the reason this one writes cleanly — refuting the section consumes a CoList-equality; building the iso would assert one. The unwritability is the not-epi face's other coat: structurally the observer's to perform, never the proof's.
🤖 Generated with Claude Code