Skip to content

docs(r3): Q-MachineConstraint follow-on — Compose<concept> + cost-lens unification (post-#1817) - #1821

Merged
briansrls merged 10 commits into
mainfrom
docs/q-machine-constraint-ratification-2026-05-06
May 6, 2026
Merged

docs(r3): Q-MachineConstraint follow-on — Compose<concept> + cost-lens unification (post-#1817)#1821
briansrls merged 10 commits into
mainfrom
docs/q-machine-constraint-ratification-2026-05-06

Conversation

@briansrls

@briansrls briansrls commented May 6, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

Follow-on to merged PR #1817 (Q-MachineConstraint-Carrier RATIFIED). Captures three commits that landed on the branch after #1817's squash-merge:

  1. 150c28aa4 — codex BLOCKING fix: sub-decision 3 reframed from Compose<AbelianGroup, MachineWidth<64>> (witness-shape in slot-1, type-error per dsl/std/algebra.dag:148-150) to Compose<Int, MachineWidth<64>> (algebraic concept in slot-1). Sub-decision 4 follows: Compose<Real, MachineWidth<64>>.

  2. a00010c12 — sub-decision 6 unified with T-CostLens-Composition per Brian directive ("basically this would be represented by cost right — in all cases we should be able to represent the structure with literal bits/objects or whatever — the cost would be enormous"). Universality of faithful representation + cost lens as discriminator + Grounding picks lowest-cost faithful representation. Implication: existing docs/design-numeric-construction.md:194-198 Python row (Nat<N> → int with size-hint metadata) is non-faithful (drops structure; cost lens can't read it); routes to T-Numeric-Construction / Grounding lane paydown to install cost-tiered faithful-representation table.

(Plus 694db2ea1 Python-divergence callout — superseded by a00010c12's cost-lens reframe but the file content is consistent.)

Why this is a follow-on PR

#1817 was squash-merged before these three commits landed on the branch. The squash captured 8099ace90 (claude APPROVE observations applied) but not the subsequent codex BLOCKING fix or cost-lens unification. This PR brings main up to the latest correct framing.

Files changed

File Change
docs/r3-design-schedule-2026-05-06.md §S3 sub-decisions 3, 4, 6 reframed (Compose; Compose; cost-lens-as-discriminator)
docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row matching sub-decisions 3, 4, 6 reframe in canonical authority

Test plan

  • Sub-decision 3 spelling matches dsl/std/algebra.dag:148-150 carrier-vs-witness distinction (algebraic concept in slot-1 of Compose<...>)
  • Sub-decision 4 uses fully-applied Real (= ApproximateField<Rational>), not bare ApproximateField constructor
  • Sub-decision 6 cross-references T-CostLens-Composition gates (cost_lens_reads_target_realization, coercion_cost_equals_complexity_by_construction)
  • Wrong forms retained as anti-references with explicit "prior phrasing was wrong" framing
  • Python-divergence reframed as cost-lens-paydown (existing design-numeric-construction.md row is non-faithful, not a competing default)

🤖 Generated with Claude Code

briansrls and others added 10 commits May 6, 2026 06:03
@briansrls @claude
docs(r3): Q-MachineConstraint-Carrier RATIFIED — universal substrate …
64ebf28 
…+ 5 PM defaults (Brian directive)

Brian directive 2026-05-06: "universal substrate, ratify defaults".

Resolves Q-MachineConstraint-Carrier (was OPEN per r3-program-plan.md §10.3)
with 6 sub-decisions ratified:

1. Axes in R3 scope: MachineWidth<bits> only. RegisterClass<R> / EndianMode<E>
   / alignment / signedness-as-axis deferred post-R3.
2. Interaction substrate shape: parametric Compose<Algebra, MachineConstraint>
   type-level construction. Closed-enumeration lookup-maps rejected (bridges).
3. Type-level spelling: Int<64> = Compose<AbelianGroup, MachineWidth<64>>
   parametrically. Equivalent under both algebra-side options per PR #1815.
4. Approximate-algebra layering: algebra approx + machine approx are
   independent composing axes. Real<64> = Compose<ApproximateField<Rational>,
   MachineWidth<64>> carries both layers per S8 discipline.
5. Class 1 demonstration breadth: ≥3 algebra×constraint pairs is minimum,
   not target. Broader coverage follows automatically once parser handles
   generic interaction syntax.
6. Target-specificity: MachineConstraint<C> is UNIVERSAL substrate (Brian
   directive). Every target carries machine-constraint facts as substrate;
   targets lacking native machine-width semantics (Python int/float) handle
   omission at Grounding-level discharge — target-conditioned lowering,
   NOT target-conditioned substrate.

Substrate Mgr S3 dispatch unblocked on machine-constraint side; independent
of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815
(interaction semantics carries through under either).

Updates:
- docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row: OPEN →
  RATIFIED 2026-05-06 with all 6 sub-decisions named.
- docs/r3-design-schedule-2026-05-06.md §S3: drops "open scope" framing;
  explicit ratified-scope block citing the 6 decisions; S3 dispatch noted
  as unblocked on machine-constraint side.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): Q-MachineConstraint sub-decisions 1/2/5/6 elaborated per Br…
8f5483b 
…ian clarifying inline

Brian clarifying directive 2026-05-06 on the 6 sub-decisions:

1. AXES — accept MachineWidth<bits> only; add separation-of-facts/concerns
   discipline note: algebra/machine-constraint/target-lowering are distinct
   axes. Integer modeling is the canonical exercise.

2. INTERACTION SHAPE (revised from "parametric Compose<...>" framing):
   "these models interact a la rest apis interacting — scalable / no dual
   representations (.dag generated)". The interaction substrate is
   .dag-DECLARED + .dag-GENERATED, never hand-coded. Hard constraint: no
   dual representations — any Rust counterpart must be generated, never
   hand-maintained (feedback_isomorphism_or_generation_for_mirrors +
   feedback_no_generated_code_on_disk).

3. SPELLING — Compose<AbelianGroup, MachineWidth<64>> ratified ("ok fine").
   Note added: the interaction substrate elaborating Compose<...> is
   .dag-generated per sub-decision 2.

4. LAYERING — independent composing axes ratified ("ok fine"). Real<64> =
   Compose<ApproximateField<Rational>, MachineWidth<64>> stays.

5. DEMONSTRATION BREADTH — strengthened: "3 is not a target, we shouldn't
   be 'targeting' modeling, we are just doing our best job to faithfully
   represent the concepts". Closure criterion is "concept is faithfully
   modeled", not "≥3 pairs land". 3-pair demonstration is minimum
   existence proof, not closure target.

6. TARGET-SPECIFICITY — universal substrate stays. Python lowering uses
   faithful target-available primitives (numpy.uint8 / ctypes.c_uint8 /
   explicit literal-bits), NOT omission. "if python lacks — we would have
   to actually represent the struct using something that python faithfully
   provides — i.e. either literal bits or otherwise". Faithful
   representation > target-conditioned omission.

Updates docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row +
docs/r3-design-schedule-2026-05-06.md §S3 ratified-scope block to reflect
clarifying inline.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
Merge remote-tracking branch 'origin/main' into docs/q-machine-constr…
83be121 
…aint-ratification-2026-05-06
@briansrls @claude
docs(r3): closure predicate aligned to faithful-modeling criterion (o…
e1ea7cf 
…penai-pro BLOCKING fix)

openai-pro REQUEST_CHANGES at sha 8f5483b on PR #1817 caught a real
internal inconsistency: ratification text said "Faithful representation of
the concept is the closure criterion; pair-counting is not" but the actual
closure predicates across r3-structure.md / r3-program-plan.md /
r3-design-schedule-2026-05-06.md still phrased Pass as "≥3 pairs emit to
target primitives". This violated single-authority + facts-flow-forward.

Fix: align all 5 Pass-condition / closure-predicate locations to the
faithful-modeling criterion ratified in Q-MachineConstraint sub-decision 5:

- docs/r3-program-plan.md:74 (gate #60 Pass condition in §1.4 ledger):
  "Gate Pass = concept faithfully modeled (per Brian directive 2026-05-06)
  — once substrate carries algebra + machine-constraint as independent
  composing axes with .dag-generated interaction substrate, all valid pairs
  work by construction. Minimum existence-proof evidence: 3 pairs lower
  without v2-fallback (evidence, not target)."
- docs/r3-program-plan.md:257 (§1.8 canonical ledger row): "concept
  faithfully modeled... min existence-proof = Int<64>/Real<64>/Nat<8>
  lower without v2-fallback (evidence, not target)"
- docs/r3-program-plan.md:430 (§1.4 Class 1 representative gap-test):
  "Representative gap-test (minimum existence-proof, NOT target) — substrate
  faithfully modeling algebra + machine-constraint separation IS the
  closure criterion; the 3 pairs below are the minimum existence-proof"
- docs/r3-structure.md:173 (canonical gate description): "Pass condition:
  concept faithfully modeled... Minimum existence-proof evidence (not
  closure target): 3 pairs lower without v2-fallback"
- docs/r3-design-schedule-2026-05-06.md:60 (S3 closure predicate cite):
  "Pass = concept faithfully modeled... 3-pair set is minimum
  existence-proof evidence, NOT the closure target"

Sub-decision 5 explanatory text retains "≥3 pairs land" as anti-reference
to the prior phrasing for traceability of the change.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): apply 2 claude APPROVE-with-observations precisions on Q-Ma…
8099ace 
…chineConstraint

Claude review at sha e1ea7cf (post-BLOCKING-fix) APPROVE with two
exploratory observations. Both worth applying:

1. Sub-decision 3: clarify Compose<...> elaboration vs interaction substrate.
   Sub-decision 2 says the *interaction substrate* (composition/projection/
   coercion machinery) is .dag-generated, not the Compose<...> type itself.
   Avoid an S3 worker reading "the Compose type is generated."

2. Closure predicate: explicit note that §1.4 conjunctive-closure rule still
   binds. Sub-decision 5 narrows what counts as Pass (concept faithfully
   modeled, not pair-counting), but does NOT relax the conjunctive form
   (representative gap-test executes AND class-bridge enumeration = 0).

Both are tightening clarifications; no disposition change.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
Merge remote-tracking branch 'origin/main' into docs/q-machine-constr…
a813097 
…aint-ratification-2026-05-06
@briansrls @claude
docs(r3): codex BLOCKING fix — Compose<concept, MachineWidth<...>> no…
150c28a 
…t Compose<witness, ...>

Codex BLOCKING at sha 8099ace on PR #1817 caught a real type-level error:
Compose<AbelianGroup, MachineWidth<64>> composes the *algebra witness shape*
rather than the integer carrier. Per dsl/std/algebra.dag:148-150:

  "T = GroupCompletion<M> is the carrier; AbelianGroup<T> carries
   op/identity/inverse over that carrier"

AbelianGroup<T> is a witness shape generic over carrier T, not a carrier
constructor. The bare AbelianGroup (without args) is just the kind/
constructor — putting it in Compose<...> slot-1 doesn't yield an integer
carrier.

Correct form: first slot of Compose<...> holds the **algebraic concept**
(the fully-applied carrier+witness composite that IS the Int / UInt /
Real / Nat type), second slot holds the machine-constraint:

- Int<64>  = Compose<Int, MachineWidth<64>>      (Int = AbelianGroup<GroupCompletion<Nat>> per #1466)
- UInt<64> = Compose<UInt, MachineWidth<64>>     (UInt = CommutativeMonoid<Nat> per #1818)
- Real<64> = Compose<Real, MachineWidth<64>>     (Real = ApproximateField<Rational>)
- Nat<8>   = Compose<Nat, MachineWidth<8>>

Updates sub-decision 3 (type-level spelling) + sub-decision 4 (approximate-
algebra layering) in both r3-design-schedule-2026-05-06.md §S3 and
r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row. Wrong-form
references retained as anti-references only ("prior phrasing was wrong";
critical correction note + dsl/std/algebra.dag citation).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): flag Python width-lowering divergence with design-numeric-c…
694db2e 
…onstruction.md (codex non-blocking)

Codex non-blocking improvement at sha 83be121: sub-decision 6's Python
faithful-lowering directive (numpy.uint8 / ctypes.c_uint8 / literal-bits)
competes with the existing default at docs/design-numeric-construction.md:
194-198 which lowers Nat<N> for any N to plain Python int with size-hint
metadata (width-omission default).

Brian's directive ("represent the struct using something that python
faithfully provides") shifts the standing default to faithful concrete
representation, but the existing design doc isn't updated yet.

Fix: explicit "Tracked divergence" callout in sub-decision 6 (both r3-design-
schedule.md §S3 and r3-program-plan.md §10.3 row). Routes reconciliation
to T-Numeric-Construction / Grounding lane paydown — update
design-numeric-construction.md Python row when the Grounding-side per-target
lowering authority lands. Not bundled in this PR per scope; the divergence
is tracked-not-silent.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): sub-decision 6 unified with cost lens — universal faithful …
a00010c 
…representation, cost as discriminator (Brian directive)

Brian directive 2026-05-06 elaborated 2x:
"basically this would be represented by cost right - in all cases we
should be able to represent the structure with literal bits/objects or
whatever - the cost would be enormous - in those cases, we would look for
alternatives like better modeling/libraries/int & 0xFF"

This unifies sub-decision 6 with T-CostLens-Composition: faithful
representation is universal (every target CAN represent every concept,
literal-bits is the always-available floor); the cost lens is the
discriminator that orders the alternatives.

Reframing:

- Universality of faithful representation: every target carries every
  concept faithfully (literal-bits as the floor)
- Cost lens (T-CostLens-Composition gates cost_lens_reads_target_realization
  + coercion_cost_equals_complexity_by_construction) reads per-primitive
  realization cost from target language spec
- Grounding selects the lowest-cost faithful representation by reading
  cost-lens output
- For Python u8: cost-tier 1 = numpy.uint8 (low cost), cost-tier 2 =
  ctypes.c_uint8 (medium), cost-tier 3 = int & 0xFF discipline (universal
  floor, high cost). All three faithful; cost lens orders.

Implication: existing docs/design-numeric-construction.md:194-198 Python
row (Nat<N> → int with size-hint metadata) is NON-FAITHFUL — drops width
structure to opaque metadata, cost lens cannot read what isn't there.
Reframe routes to T-Numeric-Construction / Grounding lane paydown:
replace with cost-tiered faithful-representation table.

This is the structurally-elegant unification: faithful-representation
universality + cost-lens-as-discriminator. Sub-decision 6 IS an instance
of "coercion cost = complexity by construction" thesis (T-CostLens-Composition
load-bearing claim).

Updates both r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md
§10.3 Q-MachineConstraint-Carrier row sub-decision 6.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
Merge remote-tracking branch 'origin/main' into docs/q-machine-constr…
b9f69e6 
…aint-ratification-2026-05-06
@briansrls
briansrls marked this pull request as ready for review May 6, 2026 06:48
@briansrls briansrls changed the title Gunbc PM docs(r3): Q-MachineConstraint follow-on — Compose<concept> + cost-lens unification (post-#1817) May 6, 2026
@briansrls

briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: b9f69e6a · Trigger: schedule
  • Comparison: origin/main @ da77396b ... review/pr-1821-b9f69e6a @ b9f69e6a
  • Thinking: 13s wall

Docs-only PR correcting the Compose<...> slot-1 spelling and adding a cost-lens framing. Diff is internally consistent.

Verdict: APPROVE — Documentation-only change to two design docs. The correction (Compose<AbelianGroup, MachineWidth<64>> → Compose<Int, MachineWidth<64>>) is well-grounded in the cited dsl/std/algebra.dag:148-150 distinction between witness shape and carrier, and the cost-lens framing for sub-decision 6 is consistently applied across both files. The implication note for docs/design-numeric-construction.md:194-198 is explicitly tracked-not-silent and routed to the appropriate lane rather than bundled here, which respects scope discipline. No INVARIANTS / modeling-discipline / CODING / TESTING violations to flag — no code or .dag substrate changes in this diff.

@briansrls

briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor Author

Re: claude APPROVE at b9f69e6a — noted

APPROVE with no findings; verdict cites all three load-bearing aspects of this follow-on:

  • Compose → Compose correction grounded in dsl/std/algebra.dag:148-150
  • Cost-lens framing applied consistently across r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md §10.3 row
  • design-numeric-construction.md:194-198 implication "tracked-not-silent and routed to appropriate lane rather than bundled here, which respects scope discipline"

No further action. PR stands ready for merge.

— sent from deep-wolf-155

@briansrls
briansrls merged commit 6a6eaba into main May 6, 2026
7 checks passed
@briansrls briansrls mentioned this pull request May 6, 2026
Closed
@briansrls
briansrls deleted the docs/q-machine-constraint-ratification-2026-05-06 branch June 1, 2026 18:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@briansrls