Skip to content

Add visual manual and organize Proof Atlas in the site's scientific style - #127

Merged
moiseevigor merged 5 commits into
masterfrom
feat/proof-atlas-visual-manual
Oct 24, 2026
Merged

moiseevigor merged 5 commits into
masterfrom
feat/proof-atlas-visual-manual

Conversation

@moiseevigor

@moiseevigor moiseevigor commented Oct 24, 2026 •

Copy link
Copy Markdown
Owner

Proof Atlas mixed a separate green palette, a scattered constructor reference and a long chronological implementation record. This change gives it the blog's scientific article styling and one reading route: notation → compiled proof explorer → research program. Detailed checks are searchable in a separate evidence index. The Projects list becomes a borderless editorial list.

The new visual manual covers all 12 Expr forms and 27 semantic fields, lexical scope, sharing, exact cuts, folding, typed construction schemata and universe/source boundaries. Its four interactive controls use the production scene model and explicitly have no native typing certificate. The older constructor gallery now preserves every semantic field, including all three letE children.

The manual, grammar, readers and canvases share Source Serif 4, IBM Plex Sans, IBM Plex Mono and the site theme tokens. Eight manual rules use the existing KaTeX renderer. Canvas themes update live without changing source selections; relation labels, line styles and glyphs remain explicit. The Projects list removes repeated separators, badges and the third-party button widget.

The canonical program retains its goal and representation contract, with a short reading route, capability table and open questions. All 63 former technical sections are preserved verbatim, grouped into five research layers. All 75 old section anchors remain available; old program fragment links forward to the preserved evidence sections. The published research post and mathematical manuscript source are unchanged.

Validation:

  • 63-section content preservation SHA-256: f467d72dbda2e3f853c9dcd69715ee37f41b8e55ac192db87162fd59213ba2f7.
  • Manual field/scope controls: 80 cuts, 60 lexical links and 81 rejection controls.
  • New browser audit: 34 responsive states (320/390/820/1440 widths), 20 accessibility audits, eight rendered math figures, all 75 anchor targets, representative forwarding, search/layer filters and four live canvas theme states with unchanged selections.
  • Existing manual, microscope, scoped geometry, telescopes, applications, 74-entry language reference, complete syntax-count, article correspondence and synchronized-reader regressions pass. The synchronized reader checks 84 exact path bridges and preserves 916 rendered article formulas. The final count browser checks all 269 frames and 1,430 annotations, including failure recovery and stale-selection controls.
  • All 58 browser suites from the context-accounting checkpoint through the manual pass locally after the touch-target fix.
  • Production build and exact source/build asset comparisons are retained in task evidence. Browser tests join the existing CI workflow; no native compiler job or external dependency is added.

No compiled proof packet, native query, original Lean source, mathematical article or blog post is changed. This establishes presentation/navigation fidelity, not improved proof comprehension or a completed semantic language.

Depends on the compiled-count release in #126, now merged. The final navigation regressions cover the four-entry Projects list, ordered Atlas route, legacy evidence redirects, keyboard scrolling of retained rules and universe controls (including corrupt/missing optional fixtures).

The shared theme preserves the existing 44-pixel interaction targets in context-accounting, context-interface, scope and witness controls. The full browser regression caught a more-specific theme rule reducing those targets; the fix retains the existing assertions.

Deployed in merge 0d991e84b88b657935db8568bd68703bedde6c79 after all seven exact-head checks passed. The actual merge tree matches the tested tree. Pages deployment succeeded for that merge.

Hosted verification passed all 14 browser suites and compared all 4,252 updated count/runtime assets byte-for-byte with the tested release. This includes 269 syntax-count frames / 1,430 annotations, 84 article path bridges, desktop/phone and both-theme checks.

Live: Proof Atlas · Visual manual · Projects.

@moiseevigor moiseevigor changed the title Add visual proof manual and preserve every constructor field Add visual manual and organize Proof Atlas in the site's scientific style Oct 24, 2026
@moiseevigor
moiseevigor marked this pull request as ready for review October 24, 2026 18:40
@moiseevigor
moiseevigor changed the base branch from feat/proof-atlas-free-index-multiplicity to master October 24, 2026 18:40
@moiseevigor
moiseevigor merged commit 0d991e8 into master Oct 24, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant