verify: math-specific glossary layout (Sprint 3 of v0.5+ expansion)#43
Merged
Conversation
…+ Mathlib bridge callouts + Lean coverage unified)
Sprint 3 of the verify-lane v3 backlog future-work. The math glossary
now renders with a proof-style layout tailored to mathematical content,
distinct from the physics SI cascade / life biomarker / metaphysics
phenomenological sections.
Layout (`_layouts/glossary-entry.html`):
- Adds a new Section 3 branch for `domain == "mathematics"` rendering
`mathematical_content` with:
* theorem-statement box (highlighted, proof-style block) with
per-`kind` colour accent (theorem / lemma / definition / postulate /
axiom / structure / object).
* Exact + decimal value fields for definitions like ι_τ.
* Collapsible proof sketch (`<details class="deep-dive math-proof-sketch">`).
* Rationale paragraphs (uniqueness, role, non-ω qualifier, etc.).
* Consequences / load-bearing values / load-bearing pairs lists.
* Mathlib bridge callout (`<aside class="mathlib-bridge-callout">`).
- Unifies the Lean Coverage section: physics/life/metaphysics use
`lean_coverage`; mathematics uses `lean` (mirroring registry shape).
The section now reads `lean_coverage | default: lean` so both render.
Module name is hyperlinked to the GitHub source at the pinned commit.
SCSS (`_sass/_components.scss`):
- `.theorem-statement-box` with 7 per-kind accent variants
- `.mathlib-bridge-callout` (highlighted aside)
- `.chip-math-kind-{theorem,lemma,...}` colour palette
- `.chip-math-symbol` (italic serif)
- `.math-glossary-content` collapsible-proof-sketch styling
- Mobile breakpoint at 760px
Data (`_data/glossary/*.json`):
- Refreshed from corpus#23 (which fixed the public-payload allowlist
to expose `mathematical_content` + `lean` for math entries).
Verification:
- bundle exec jekyll build → exit 0, done in 536s
- grep -c "theorem-statement-box|mathlib-bridge-callout|chip-math-kind"
_site/results/mathematics/glossary/MathG-T04-central-theorem/index.html → 5
- grep -c "theorem-statement-box"
_site/results/physics/glossary/PG-C02-iota-tau/index.html → 0 (no spillover)
- TauLib module hyperlinks render on every math entry's Lean section.
Depends on Panta-Rhei-Research/corpus#23 (already merged).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
AnSoFuchs
approved these changes
May 2, 2026
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
2 participants
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.
Summary
Sprint 3 of the verify-lane v3 backlog future-work. The math glossary now renders with a proof-style layout tailored to mathematical content, distinct from the physics SI cascade / life biomarker / metaphysics phenomenological sections.
What changed
_layouts/glossary-entry.html— new `domain == "mathematics"` Section 3 branch:Details
`.Plus unifies the Lean Coverage section across all 4 domains: physics/life/metaphysics' `lean_coverage` and mathematics' `lean` (registry-mirroring shape) both render via `lean_coverage | default: lean`. Module names now hyperlink to the GitHub source at the pinned commit.
_sass/_components.scss— new SCSS classes:_data/glossary/*.json— refreshed from corpus#23.Verification
Dependency
Requires Panta-Rhei-Research/corpus#23 (data fix exposing `mathematical_content` + `lean` in public payload — already merged).
Sprint position
Final sprint of three planned waves. The verify-lane v3 future-work is now closed:
🤖 Generated with Claude Code