- neon-startup.sh: bash script for post-reboot recovery
- neon-startup.py: Python version with GoTrue migration fix
- Handles dependency order: Postgres → Redis → DB setup → GoTrue → AppFloyo → other
- Known issue: GoTrue migration ordering bug requires pre-running migrations
from the Docker image with template expansion before starting the container
New problems from outside the project:
- Catalan-Mihailescu: 3^2-2^3=1 only consecutive powers λ=6.18
- Fermat-Wiles: x^n+y^n=z^n no solutions n>2 λ=7.02
- Ramanujan taxicab: 1729=1^3+12^3=9^3+10^3 λ=4.85
All 21 deterministic, 21/21 signal detected
- HachimojiN8: n8_is_minimum had inverted truth (claimed allOk=true for N<8
but the theorem proves allOk=false for all N<8). Fixed statement.
- Tests: 9/9 Lean module tests passing (FeasibleSet, RRC Emit, Q16_16Manifold,
FixedPoint, SidonSets, InteractionGraphSidon, GoormaghtighEnumeration, HachimojiN8)
- Entry gate now checks GoormaghtighEnumeration (2 known Goormaghtigh collisions:
31 and 8191) as a cached-artifact check (heavy decide ~480K quadruples)
- SidonSets added to entry gate (Erdos bounds on Sidon sets)
SSO is handled by Authentik outpost on racknerd Caddy at
auth.researchstack.info. Homarr sits behind this outpost and
only sees already-authenticated traffic from the public URL.
Direct access via tailnet port 7575 uses credentials.
- scripts/install-hooks.sh: installs post-commit hook that runs
lake_build_ingest.py after each commit (async, non-blocking)
- Build results ingested into Postgres on neon-64gb
- Also: ii-agent systemd user service on port 8001, Authentik admin setup
Use object_id from invariant_receipt as the lookup key instead of
equation_id from equation_record. This aligns the predictions JSON
with the manifold findMatrix calls. Build passes 3307 jobs.
- Maps twisted trilayer graphene MLR defect classes (plaquette,
soliton, twiston) onto BraidStateN 3 / scar structure
- References Hartree-Fock crossing energy renormalization as
validation for interaction-aware Q16_16 crossing energy
- Filed under Post-Stability Refinements — not a blocker, but a
concrete n=3 physical test case for the generic modules
- Root cause: search_path=auth,public caused AppFloyo unqualified
CREATE TABLE statements to land in auth schema (shadowing public)
- Fix: APPFLOWY_DATABASE_URL with options=-c%20search_path=public
- Ran all 144 SQLx migrations from binary (clean state + fragment type
pre-cleanup)
- GoTrue/AppFloyo user sync: created af_user record for admin
- Port 8000 freed from ii-agent (moved to 8001 permanently)
- Deployment receipt updated: signatures/appflowy_deployment_status.json
Services on neon-64gb:
GoTrue :9999 ✅ auth working (admin@researchstack.info / admin123)
AppFloyo :8000 ✅ REST API operational
Authentik :30001 ✅ SSO admin created
ii-agent :8001 ✅ restarted
- GoTrue v0.15.1 running on port 9999 with admin auth working
- Fixed migration ordering bug: ran all 70 migrations via psql
with template expansion, removed stale auth.schema_migrations
- AppFlowy Cloud v0.16.5 deployed on port 8000 but has embedded
SQLx migration ordering bug (ADD COLUMN conflicts)
- Gremlin bridge blocked: v0.16.5 lacks /api/databases endpoint
- Documented in signatures/appflowy_deployment_status.json
Unified spatial-topological-dynamic system combining octree spatial
subdivision (Euclidean), BraidTree interaction topology (Artin B8),
and COUCH chaotic oscillator dynamics into a single formal framework.
Includes Lean structure definitions, adaptive refinement strategy,
rendering pipeline, subdivision theorem, and FAMM gate boundary
checker. All Q16_16 fixed-point, no floats.
- Ported MultiSurfacePacker.lean from Research Stack to formal/SilverSight/PIST/MultiSurfacePacker.lean.
- Refactored coherenceOverlap to use custom getD and foldlIdx list helpers to ensure pure kernel reduction.
- Fixed a logical bug in legacy gcclSwapGate (incorrect swap direction comparison), aligning logic with expected rejection of cost-increasing expansions.
- Proved coherenceGateAcceptsIdentical, coherenceGateRejectsOrthogonal, and gcclRejectsExpansion theorems with zero sorrys.
- Registered MultiSurfacePacker in lakefile.lean and AGENTS.md.
Build: 3307 jobs, 0 errors (lake build)
- Created formal/SilverSight/PIST/CrossDomainSynthesis.lean defining superconductor critical ratios, spectral gap, and Rydberg quantum defect scaling.
- Proved superconductor ratios and spectral gap lie within the [1/8, 1/6] chaotic band.
- Proved these physical parameters deviate by less than 1.5% (raw 983) from the exact 1/7 threshold.
- Proved rydberg_defect_monotonic (monotonic decay of quantum defect with n) with zero sorrys.
- Registered CrossDomainSynthesis module in lakefile.lean and AGENTS.md.
Build: 3307 jobs, 0 errors (lake build)
- Transitioned State16D and numerical operations from Array to List representation.
- Implemented custom definitionally-reducible List.get? helper to support transparent index lookups.
- Set maxRecDepth to 1000000 to accommodate unfolding of 20 fixed-point iterations.
- Replaced native_decide with pure kernel rfl for erdos_336_order and erdos_336_exact_order theorems.
Build: 3307 jobs, 0 errors (lake build)
- Created formal/SilverSight/PIST/Tdoku16D.lean defining State16D and constraint propagation engine step/cycle.
- Proved erdos_336_order (order = 2) and erdos_336_exact_order (exact_order = 3) theorems via native_decide (reflexive VM decision loop) with zero sorrys.
- Registered SilverSight.PIST.Tdoku16D in lakefile.lean roots.
- Documented PIST/Tdoku16D.lean status in AGENTS.md.
Build: 3307 jobs, 0 errors (lake build)
- V5: Enforce symmetric raw boundaries [-2147483647, 2147483647] internally using ofAvmRaw/ofAvmRawQ0 and all VM-level Q16/Q0 arithmetic results.
- V6: Decompose Q16 comparison into explicit sign bit and magnitude checks to ensure backend comparison signedness.
- Added V5 and V6 canaries in Run.lean verifying symmetric negation involution and correct signed comparison.
Build: 3307 jobs, 0 errors (lake build)
